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 metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00920496
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, December 18, 2013 - 3:41:00 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Wednesday, March 19, 2014 - 5:51:46 AM

File

TushkanovaRGK-ADDCT13.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00920496, version 1

Citation

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⟩

Share

Metrics

Record views

364

Files downloads

117