HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

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 metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00703207
Contributor : Claire Dross Connect in order to contact the contributor
Submitted on : Friday, June 1, 2012 - 10:50:04 AM
Last modification on : Friday, February 4, 2022 - 3:30:05 AM
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

Citation

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

Share

Metrics

Record views

256

Files downloads

171