Reasoning with Triggers

Claire Dross 1, 2, * Sylvain Conchon 1, 2 Andrei Paskevich 1, 2
* Auteur correspondant
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.
Type de document :
[Research Report] RR-7986, INRIA. 2012, pp.29
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger
Contributeur : Claire Dross <>
Soumis le : vendredi 1 juin 2012 - 10:50:04
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 30 novembre 2012 - 13:10:29


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers