Skip to Main content Skip to Navigation
New interface
Journal articles

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, April 18, 2011 - 6:48:35 PM
Last modification on : Friday, November 18, 2022 - 9:26:57 AM

Links full text



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



Record views