Abstract canonical presentations

Nachum Dershowitz Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Solving goals -- like proving properties, deciding word problems or resolving constraints -- is much easier with some presentations of the underlying theory than with others. Typically, what have been called "completion processes", in particular in the study of equational logic, involve finding appropriate presentations of a given theory to more easily solve a given class of problems. We provide a general proof-theoretic setting that relies directly on the fundamental concept of "good", that is, normal-form, proofs, itself defined using well-founded orderings on proof objects. This foundational framework allows for abstract definitions of canonical presentations and very general characterizations of saturation and redundancy criteria.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2006, Theoretical Computer Science, 357 (1-3), pp.53--69. 〈10.1016/j.tcs.2006.03.012〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00121760
Contributeur : Claude Kirchner <>
Soumis le : jeudi 21 décembre 2006 - 18:35:56
Dernière modification le : jeudi 17 mai 2018 - 12:52:03

Lien texte intégral

Identifiants

Collections

Citation

Nachum Dershowitz, Claude Kirchner. Abstract canonical presentations. Theoretical Computer Science, Elsevier, 2006, Theoretical Computer Science, 357 (1-3), pp.53--69. 〈10.1016/j.tcs.2006.03.012〉. 〈inria-00121760〉

Partager

Métriques

Consultations de la notice

123