Pubblicazioni

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

Autori:
Bonacina, Maria Paola; Christopher A., Lynch; Leonardo de, Moura
Titolo:
On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving
Anno:
2009
Tipologia prodotto:
Contributo in volume (Capitolo o Saggio)
Tipologia ANVUR:
Contributo in volume (Capitolo o Saggio)
Lingua:
Inglese
Formato:
A Stampa
Titolo libro:
Automated Deduction - CADE 22 - 22nd International Conference on Automated Deduction- Montreal, Canada, August 2009 - Proceedings
Casa editrice:
Springer
ISBN:
9783642029585
Intervallo pagine:
35-50
Parole chiave:
Software verification; Satisfiability modulo theories; Decision procedures; Superposition-based inference systems
Breve descrizione dei contenuti:
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.
Pagina Web:
http://dx.doi.org/10.1007/978-3-642-02959-2_3
https://mariapaola.github.io/
Id prodotto:
114332
Handle IRIS:
11562/328430
depositato il:
26 marzo 2012
ultima modifica:
16 settembre 2023
Citazione bibliografica:
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 - Proceedings2009Springer2009pp. 35-50

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

<<indietro

Attività

Strutture

Condividi