A Completion Method to Decide Reachability in Rewrite Systems

Abstract : The Knuth-Bendix method takes in argument a finite set of equations and rewrite rules and, when it succeeds, returns an algorithm to decide if a term is equivalent to another modulo these equations and rules. In this paper, we design a similar method that takes in argument a finite set of rewrite rules and, when it succeeds, returns an algorithm to decide not equivalence but reachability modulo these rules, that is if a term reduces to another. As an application, we give new proofs of the decidability of reachability in finite ground rewrite systems and in pushdown systems.
Type de document :
Communication dans un congrès
Carsten Lutz; Silvio Ranise. International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.205-219, 2015, Lecture Notes in Computer Science. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_13〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01252138
Contributeur : Gilles Dowek <>
Soumis le : jeudi 7 janvier 2016 - 11:56:39
Dernière modification le : mardi 13 novembre 2018 - 17:10:03
Document(s) archivé(s) le : vendredi 8 avril 2016 - 13:19:54

Fichiers

pkb.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Burel, Gilles Dowek, Ying Jiang. A Completion Method to Decide Reachability in Rewrite Systems. Carsten Lutz; Silvio Ranise. International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.205-219, 2015, Lecture Notes in Computer Science. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_13〉. 〈hal-01252138〉

Partager

Métriques

Consultations de la notice

192

Téléchargements de fichiers

68