Diagrammatic Confluence and Completion

Jean-Pierre Jouannaud 1 Vincent Van Oostrom
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : We give a new elegant proof that decreasing diagrams imply confluence based on a proof reduction technique, which is then the basis of a novel completion method which proof-reduction relation transforms arbitrary proofs into rewrite proofs even in presence of non-terminating reductions. Unlike previous methods, no ordering of the set of terms is required, but can be used if available. Unlike ordered completion, rewrite proofs are closed under instantiation. Examples are presented, including Kleene's and Huet's classical examples showing that non-terminating local-confluent relations may not be confluent.
Type de document :
Communication dans un congrès
Wolfgang Thomas. International Conference in Automata, Languages and Programming, Jul 2009, Rhodes, Greece. Springer Berlin/Heidelberg, 2, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02930-1〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00436070
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : jeudi 26 novembre 2009 - 08:30:52
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29

Identifiants

Collections

Citation

Jean-Pierre Jouannaud, Vincent Van Oostrom. Diagrammatic Confluence and Completion. Wolfgang Thomas. International Conference in Automata, Languages and Programming, Jul 2009, Rhodes, Greece. Springer Berlin/Heidelberg, 2, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02930-1〉. 〈inria-00436070〉

Partager

Métriques

Consultations de la notice

168