Automatic Decidability and Combinability Revisited

Christopher Lynch 1 Duc-Khanh Tran 2
2 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present an inference system for clauses with ordering constraints, called Schematic Paramodulation. Then we show how to use Schematic Paramodulation to reason about decidability and stable infiniteness of finitely presented theories. We establish a close connection between the two properties: if Schematic Paramodulation for a theory halts then the theory is decidable; and if, in addition, Schematic Paramodulation does not derive the trivial equality X = Y then the theory is stably infinite. Decidability and stable infiniteness of component theories are conditions required for the Nelson-Oppen combination method. Schematic Paramodulation is loosely based on Lynch-Morawska's meta-saturation but it differs in several ways. First, it uses ordering constraints instead of constant constraints. Second, inferences into constrained variables are possible in Schematic Paramodulation. Finally, Schematic Paramodulation uses a special deletion rule to deal with theories for which Lynch-Morawska's meta-saturation does not halt.
Type de document :
Communication dans un congrès
Automated Deduction - CADE-21, 2007, Bremen, Germany. Springer, 4603, pp.328-344, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73595-3_22〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00576605
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 14 mars 2011 - 17:48:10
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Christopher Lynch, Duc-Khanh Tran. Automatic Decidability and Combinability Revisited. Automated Deduction - CADE-21, 2007, Bremen, Germany. Springer, 4603, pp.328-344, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73595-3_22〉. 〈inria-00576605〉

Partager

Métriques

Consultations de la notice

85