Computing Interpolants without Proofs

Hana Chockler; Alexander Ivrii; Arie Matsliah

Computing Interpolants without Proofs

Hana Chockler, Alexander Ivrii, Arie Matsliah

IBM Israel

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

110 Downloads (Pure)

Abstract

We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕ A ∧ ϕ B , and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.

Original language	English
Title of host publication	Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers
Publisher	Springer
Pages	72-85
Number of pages	14
Volume	7857
Publication status	Published - 6 Nov 2012

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Access to Document

int

Cite this

@inbook{e6009f91bc3f4f34b51ce6e3437dc37a,

title = "Computing Interpolants without Proofs",

abstract = "We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕ A ∧ ϕ B , and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.",

author = "Hana Chockler and Alexander Ivrii and Arie Matsliah",

year = "2012",

month = nov,

day = "6",

language = "English",

volume = "7857",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "72--85",

booktitle = "Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers",

}

Computing Interpolants without Proofs. / Chockler, Hana; Ivrii, Alexander; Matsliah, Arie.
Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers. Vol. 7857 Springer, 2012. p. 72-85 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

TY - CHAP

T1 - Computing Interpolants without Proofs

AU - Chockler, Hana

AU - Ivrii, Alexander

AU - Matsliah, Arie

PY - 2012/11/6

Y1 - 2012/11/6

N2 - We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕ A ∧ ϕ B , and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.

AB - We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. In contrast with the common approaches, our method does not require a proof of unsatisfiability of ϕ A ∧ ϕ B , and can be realized using any SAT solver as a black box. We achieve this by combining model enumeration with the ability to easily generate interpolants in the special case that one of the formulas is a cube.

M3 - Conference paper

VL - 7857

T3 - Lecture Notes in Computer Science

SP - 72

EP - 85

BT - Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers

PB - Springer

ER -

Computing Interpolants without Proofs

Abstract

Publication series

Access to Document

Fingerprint

Cite this