2026-08-16T23:31:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4069 2024-03-06T10:34:47Z ddc:004 open_access

Automatic Decidability: A Schematic Calculus for Theories with Counting Operators Tushkanova, Elena Ringeissen, Christophe Giorgetti, Alain Kouchnarenko, Olga decision procedures superposition schematic saturation Many verification problems can be reduced to a satisfiability problem modulo theories. For building satisfiability procedures the rewriting-based approach uses a general calculus for equational reasoning named paramodulation. Schematic paramodulation, in turn, provides means to reason on the derivations computed by paramodulation. Until now, schematic paramodulation was only studied for standard paramodulation. We present a schematic paramodulation calculus modulo a fragment of arithmetics, namely the theory of Integer Offsets. This new schematic calculus is used to prove the decidability of the satisfiability problem for some theories equipped with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures, e.g., lists and records. An implementation within the rewriting-based Maude system constitutes a practical contribution. It enables automatic decidability proofs for theories of practical use. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Elena Tushkanova and Christophe Ringeissen and Alain Giorgetti and Olga Kouchnarenko 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.303 urn:nbn:de:0030-drops-40696 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.303 eng https://creativecommons.org/licenses/by/3.0/legalcode