Skip to Main content Skip to Navigation
New interface
Conference papers

Automatic Decidability for Theories with Counting Operators

Elena Tushkanova 1, 2 Christophe Ringeissen 1 Alain Giorgetti 1, 2 Olga Kouchnarenko 1, 2 
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The notion of schematic paramodulation has been introduced to reason on properties of (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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Wednesday, December 18, 2013 - 3:41:00 PM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM
Long-term archiving on: : Wednesday, March 19, 2014 - 5:51:46 AM


Files produced by the author(s)


  • HAL Id : hal-00920496, version 1


Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, Olga Kouchnarenko. Automatic Decidability for Theories with Counting Operators. Automated Deduction: Decidability, Complexity, Tractability (workshop ADDCT), Jun 2013, Lake Placid, United States. ⟨hal-00920496⟩



Record views


Files downloads