文章基本信息

标题：Automatic Decidability: A Schematic Calculus for Theories with Counting Operators
本地全文：下载
作者：Elena Tushkanova ; Christophe Ringeissen ; Alain Giorgetti 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：21
页码：303-318
DOI：10.4230/LIPIcs.RTA.2013.303
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：decision procedures; superposition; schematic saturation