A rule-based system for automatic decidability and combinability

Elena Tushkanova 1, 2 Alain Giorgetti 1, 2 Christophe Ringeissen 1 Olga Kouchnarenko 2, 1
1 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 : This paper deals with decision procedures specified by using a superposition calculus which is an inference system at the core of all equational theorem provers. This calculus is refutation complete: it 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 developed to build the schematic form of the saturations allowing to automatically prove decidability of single theories and of their combinations. This paper presents a rule-based logical framework and a tool implementing a complete many-sorted schematic superposition calculus for arbitrary theories. By providing results for unit theories, arbitrary theories, and also for theories with counting operators, we show that this tool is very useful to derive decidability and combinability of theories of practical interest in verification.
Document type :
Journal articles
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01102883
Contributor : Christophe Ringeissen <>
Submitted on : Thursday, January 15, 2015 - 5:35:36 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Saturday, September 12, 2015 - 6:28:30 AM

File

TGRK14.pdf
Files produced by the author(s)

Identifiers

Citation

Elena Tushkanova, Alain Giorgetti, Christophe Ringeissen, Olga Kouchnarenko. A rule-based system for automatic decidability and combinability. Science of Computer Programming, Elsevier, 2015, Selected Papers from the Ninth International Workshop on Rewriting Logic and its Applications (WRLA 2012), 99, pp.3-23. ⟨10.1016/j.scico.2014.02.005⟩. ⟨hal-01102883⟩

Share

Metrics

Record views

393

Files downloads

199