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
2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)

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.

Mots clés: Superposition; Schematic saturation; Decision procedures

Domaines: Logique en informatique [cs.LO]

Elena Tushkanova, Alain Giorgetti, Christophe Ringeissen, Olga Kouchnarenko. A rule-based system for automatic decidability and combinability. Science of Computer Programming, 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⟩