Things to know when implementing KBO

DOI10.1007/S10817-006-9031-4MaRDI QIDQ861708zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Automating the Knuth Bendix ordering
• Orienting rewrite rules with the Knuth-Bendix order.
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• scientific article; zbMATH DE number 4041334
• KBO orientability

Cites work

• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1809863 (Why is no real title available?)
• scientific article; zbMATH DE number 1765674 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Transformation System for Developing Recursive Programs
• Automated Reasoning
• Combining superposition, sorts and splitting
• Comprehending monads
• Rewriting
• The TPTP problem library. CNF release v1. 2. 1
• The loop absorption and the generalization strategies for the development of logic programs and partial deduction

Cited in

(9)

• Relaxed weighted path order in theorem proving
• scientific article; zbMATH DE number 4041334 (Why is no real title available?)
• AC-KBO revisited
• Automating the Knuth Bendix ordering
• Twee: an equational theorem prover
• Automated Reasoning
• KBO Constraint Solving Revisited
• On transfinite Knuth-Bendix orders
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties

Describes a project that uses

Uses Software

• Waldmeister
• E Theorem Prover
• TPTP
• VAMPIRE

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q861708)