Publications

Authors:

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

Title:

On deciding satisfiability by theorem proving with speculative inferences

Year:

2011

Type of item:

Articolo in Rivista

Tipologia ANVUR:

Articolo su rivista

Language:

Inglese

Format:

A Stampa

Referee:

Sì

Name of journal:

Journal of Automated Reasoning

ISSN of journal:

0168-7433

N° Volume:

47

Number or Folder:

2

:

Kluwer

Page numbers:

161-189

Keyword:

Program checking; Theorem proving; Satisfiability modulo theories; Combination of theories

Short description of contents:

Applications in software verification often require determining the satisfiability of first-order formulae with respect to 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 to be highly scalable, efficient and suitable for integrated theory reasoning. Inference systems with resolution and superposition are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a theorem-proving method that tightly integrates superposition-based inference system and SMT solver. 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 system detects any unsoundness introduced by these speculative inferences and recovers from it.

Web page:

http://dx.doi.org/10.1007/s10817-010-9213-y
https://mariapaola.github.io/

Product ID:

59335

Handle IRIS:

11562/344183

Deposited On:

July 24, 2011

Last Modified:

September 15, 2023

Bibliographic citation:

Bonacina, Maria Paola; Christopher A., Lynch; Leonardo de, Moura, On deciding satisfiability by theorem proving with speculative inferences «Journal of Automated Reasoning» , vol. 47 , n. 2 , 2011 , pp. 161-189

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