Publications

Authors:

Bonacina, Maria Paola; Christopher A., Lynch; Leonardo de, Moura

Title:

On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving

Year:

2009

Type of item:

Contributo in volume (Capitolo o Saggio)

Tipologia ANVUR:

Contributo in volume (Capitolo o Saggio)

Language:

Inglese

Format:

A Stampa

Book Title:

Automated Deduction - CADE 22 - 22nd International Conference on Automated Deduction- Montreal, Canada, August 2009 - Proceedings

Publisher:

Springer

ISBN:

9783642029585

Page numbers:

35-50

Keyword:

Software verification; Satisfiability modulo theories; Decision procedures; Superposition-based inference systems

Short description of contents:

Applications in software verification often require determining the satisfiability of first-order formulae with respect to some background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that terminates on satisfiable instances. Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory reasoning. Superposition-based inference systems are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a calculus that tightly integrates Superposition and SMT solvers. The combination is refutationally complete if background theory symbols only occur in ground formulae, and non-ground clauses are variable inactive. Termination is enforced by introducing additional axioms as hypotheses. The calculus detects any unsoundness introduced by these axioms and recovers from it.

Web page:

http://dx.doi.org/10.1007/978-3-642-02959-2_3
https://mariapaola.github.io/

Product ID:

114332

Handle IRIS:

11562/328430

Deposited On:

March 26, 2012

Last Modified:

September 16, 2023

Bibliographic citation:

Bonacina, Maria Paola; Christopher A., Lynch; Leonardo de, Moura, On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving Automated Deduction - CADE 22 - 22nd International Conference on Automated Deduction- Montreal, Canada, August 2009 - Proceedings , 2009 , Springer , 2009 , pp. 35-50

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo