Things to know when implementing KBO

DOI10.1007/s10817-006-9031-4zbMath1107.68098OpenAlexW2073351681MaRDI QIDQ861708

Bernd Löchner

Publication date: 30 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10817-006-9031-4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

An Extension of the Knuth-Bendix Ordering with LPO-Like Properties ⋮ AC-KBO revisited ⋮ Relaxed weighted path order in theorem proving ⋮ On Transfinite Knuth-Bendix Orders ⋮ Twee: an equational theorem prover

Uses Software

• VAMPIRE
• TPTP
• E Theorem Prover
• Waldmeister

Cites Work

• The TPTP problem library. CNF release v1. 2. 1
• A Transformation System for Developing Recursive Programs
• Comprehending monads
• The loop absorption and the generalization strategies for the development of logic programs and partial deduction
• Automated Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Things to know when implementing KBO