Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Claire Dross <>
Submitted on : Friday, June 1, 2012 - 10:50:04 AM
Last modification on : Wednesday, September 16, 2020 - 5:04:11 PM
Long-term archiving on: : Friday, November 30, 2012 - 1:10:29 PM


Files produced by the author(s)


  • HAL Id : hal-00703207, version 1



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



Record views


Files downloads