A Rule-Based Framework for Building Superposition-Based Decision Procedures

Elena Tushkanova 1, 2 Alain Giorgetti 2, 1 Christophe Ringeissen 2 Olga Kouchnarenko 2, 1
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper deals with decision procedures specified as inference systems. Among them we focus on superposition-based decision procedures. The superposition calculus is a refutation-complete inference system at the core of all equational theorem provers. In general this calculus provides a semi-decision procedure that halts on unsatisfiable inputs but may diverge on satisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thus it becomes a decision procedure. To reason on the superposition calculus, a schematic superposition calculus has been studied, for instance to automatically prove termination. This paper presents an implementation in Maude of these two inference systems. Thanks to this implementation we automatically derive termination of superposition for a couple of theories of interest in verification.
Type de document :
Communication dans un congrès
Franciso Durán. Rewriting Logic and Its Applications, Mar 2012, Tallinn, Estonia. Springer Berlin / Heidelberg, 7571, pp.221-239, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34005-5_12〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00749576
Contributeur : Alain Giorgetti <>
Soumis le : mercredi 7 novembre 2012 - 17:18:50
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Elena Tushkanova, Alain Giorgetti, Christophe Ringeissen, Olga Kouchnarenko. A Rule-Based Framework for Building Superposition-Based Decision Procedures. Franciso Durán. Rewriting Logic and Its Applications, Mar 2012, Tallinn, Estonia. Springer Berlin / Heidelberg, 7571, pp.221-239, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34005-5_12〉. 〈hal-00749576〉

Partager

Métriques

Consultations de la notice

183