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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01252138
Contributor : Gilles Dowek <>
Submitted on : Thursday, January 7, 2016 - 11:56:39 AM
Last modification on : Saturday, February 9, 2019 - 1:26:11 AM
Long-term archiving on : Friday, April 8, 2016 - 1:19:54 PM

Files

pkb.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Guillaume Burel, Gilles Dowek, Ying Jiang. A Completion Method to Decide Reachability in Rewrite Systems. International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. pp.205-219, ⟨10.1007/978-3-319-24246-0_13⟩. ⟨hal-01252138⟩

Share

Metrics

Record views

216

Files downloads

188