Termination Tools in Ordered Completion

DOI10.1007/978-3-642-14203-1_43zbMath1291.68376OpenAlexW1528022132MaRDI QIDQ5747788

Sarah Winkler, Aart Middeldorp

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_43

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (3)

Multi-completion with termination tools ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Completion for multiple reduction orderings
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Total termination of term rewriting is undecidable
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Multi-completion with Termination Tools (System Description)
• Equational inference, canonical proofs, and proof orderings

This page was built for publication: Termination Tools in Ordered Completion