Solving divergence in Knuth--Bendix completion by enriching signatures

DOI10.1016/0304-3975(93)90241-KzbMath0779.68051OpenAlexW2060409040WikidataQ59675416 ScholiaQ59675416MaRDI QIDQ685379

Phil Watson, Muffy Calder

Publication date: 23 January 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90241-k

zbMATH Keywords

divergence in the Knuth-Bendix completion algorithmorder sorted term rewriting

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42)

Related Items

A divergence critic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Chain properties of rule closures
• Analogical and inductive inference. International workshop AII '89, Reinhardsbrunn Castle, GDR, October 1-6, 1989. Proceedings
• Schematization of infinite sets of rewrite rules generated by divergent completion processes
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Computational aspects of an order-sorted logic with term declarations
• Inductive proofs by specification transformations
• On relationship between term rewriting systems and regular tree languages
• Divergence phenomena during completion
• Language identification in the limit
• On finite representations of infinite sequences of terms
• Meta-rule synthesis from crossed rewrite systems