Multi-completion with termination tools

DOI10.1007/s10817-012-9249-2zbMath1362.68253OpenAlexW1995618662MaRDI QIDQ352956

Masahito Kurihara, Sarah Winkler, Aart Middeldorp, Haruhiko Sato

Publication date: 5 July 2013

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

Full work available at URL: https://doi.org/10.1007/s10817-012-9249-2

zbMATH Keywords

term rewritingKnuth-Bendix completionmulti-completiontermination tools

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion ⋮ Towards automated deduction in cP systems

Uses Software

• VAMPIRE
• TPTP
• Tyrolean
• AProVE
• MU-TERM
• mkbTT
• Slothrop
• REVE

Cites Work

• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Knuth-Bendix completion of theories of commuting group endomorphisms
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• Completion for multiple reduction orderings
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Proving Termination of Context-Sensitive Rewriting with MU-TERM
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Multi-completion with Termination Tools (System Description)
• Existence, Uniqueness, and Construction of Rewrite Systems
• Equational inference, canonical proofs, and proof orderings
• AC Completion with Termination Tools
• Termination Tools in Ordered Completion
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item