1 Search Results for "Kouchnarenko, Olga"

Document
DOI: 10.4230/LIPIcs.RTA.2013.303
Automatic Decidability: A Schematic Calculus for Theories with Counting Operators

Authors: Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
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.
Cite as

Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko. Automatic Decidability: A Schematic Calculus for Theories with Counting Operators. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 303-318, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{tushkanova_et_al:LIPIcs.RTA.2013.303,
  author =	{Tushkanova, Elena and Ringeissen, Christophe and Giorgetti, Alain and Kouchnarenko, Olga},
  title =	{{Automatic Decidability: A Schematic Calculus for Theories with Counting Operators}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{303--318},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.303},
  URN =		{urn:nbn:de:0030-drops-40696},
  doi =		{10.4230/LIPIcs.RTA.2013.303},
  annote =	{Keywords: decision procedures, superposition, schematic saturation}
}
  • Refine by Author
  • 1 Giorgetti, Alain
  • 1 Kouchnarenko, Olga
  • 1 Ringeissen, Christophe
  • 1 Tushkanova, Elena

  • Refine by Classification

  • Refine by Keyword
  • 1 decision procedures
  • 1 schematic saturation
  • 1 superposition

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2013

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact