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 :
Rapport
[Research Report] RR-7986, INRIA. 2012, pp.29
Liste complète des métadonnées


https://hal.inria.fr/hal-00703207
Contributeur : Claire Dross <>
Soumis le : vendredi 1 juin 2012 - 10:50:04
Dernière modification le : jeudi 9 février 2017 - 15:56:12
Document(s) archivé(s) le : vendredi 30 novembre 2012 - 13:10:29

Fichier

RR-7986.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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>

Partager

Métriques

Consultations de
la notice

286

Téléchargements du document

139