Reasoning with Triggers

Claire Dross 1, 2, * Sylvain Conchon 1, 2 Andrei Paskevich 1, 2
* Corresponding author
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism.
Document type :
Reports
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00703207
Contributor : Claire Dross <>
Submitted on : Friday, June 1, 2012 - 10:50:04 AM
Last modification on : Thursday, April 5, 2018 - 12:30:08 PM
Long-term archiving on : Friday, November 30, 2012 - 1:10:29 PM

File

RR-7986.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00703207, version 1

Collections

Citation

Claire Dross, Sylvain Conchon, Andrei Paskevich. Reasoning with Triggers. [Research Report] RR-7986, INRIA. 2012, pp.29. ⟨hal-00703207⟩

Share

Metrics

Record views

437

Files downloads

209