|
 
|
[BDJ15] A completion method to decide reachability in rewrite systems
Conférence Internationale avec comité de lecture : 10th International Symposium on Frontiers of Combining Systems, September 2015, pp.--, Series LNAI, Wroclaw, Poland,Mots clés: rewrite system; completion; reachability; ground terms; pushdown systems
Résumé:
Knuth-Bendix method applies to a rewrite system, and, when
it succeeds, it yields an algorithm to decide if one term is equivalent
to another. In this paper, we design a similar method that, when it
succeeds, yields an algorithm to decide if one term reduces to another.
As an application, we give new proofs
of the decidability of reachability in ground rewrite systems
and in pushdown systems.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| BDJ15, | |||
| title | = | "{A completion method to decide reachability in rewrite systems}", | |
| author | = | " G. Burel and G. Dowek and Y. Jiang ", | |
| booktitle | = | "{10th International Symposium on Frontiers of Combining Systems}", | |
| year | = | 2015, | |
| month | = | "September", | |
| series | = | "LNAI", | |
| pages | = | "--", | |
| address | = | "Wroclaw, Poland", | |
| } | |||
