Automatic Decidability and Combinability

Christopher Lynch 1 Silvio Ranise 2 Christophe Ringeissen 3 Duc-Khanh Tran 4
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson-Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union? The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2011, 209 (7), pp.1026-1047. 〈10.1016/j.ic.2011.03.005〉
Liste complète des métadonnées
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 18 avril 2011 - 18:48:35
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral



Christopher Lynch, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran. Automatic Decidability and Combinability. Information and Computation, Elsevier, 2011, 209 (7), pp.1026-1047. 〈10.1016/j.ic.2011.03.005〉. 〈inria-00586936〉



Consultations de la notice