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.
Type de document :
Communication dans un congrès
Automated Deduction: Decidability, Complexity, Tractability (workshop ADDCT), Jun 2013, Lake Placid, United States. 2013
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00920496
Contributeur : Christophe Ringeissen <>
Soumis le : mercredi 18 décembre 2013 - 15:41:00
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mercredi 19 mars 2014 - 05:51:46

Fichier

TushkanovaRGK-ADDCT13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2013. 〈hal-00920496〉

Partager

Métriques

Consultations de la notice

346

Téléchargements de fichiers

94