A rule-based system for automatic decidability and combinability

• Published in: Science of computer programming 2015-03, Vol.99, p.3-23
• Main Authors: Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.
• Format: Article
• Language: English
• Subjects: Computer Science; Decision procedures; Logic in Computer Science; Schematic saturation; Superposition
• ISSN: 0167-6423; 1872-7964
• DOI: 10.1016/j.scico.2014.02.005

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. •We present a many-sorted schematic superposition calculus for non-unit theories.•The calculus is presented as a rule-based system.•The implementation automatically checks termination for some theories of interest.•Combinability of signature-disjoint theories can also be checked.