An Extension of the Knuth-Bendix Ordering with LPO-Like Properties

DOI10.1007/978-3-540-75560-9_26MaRDI QIDQ3498479zbMATH OpenOpenAlexFDO

Authors M. Ludwig, Uwe Waldmann

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_26

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• Automating the Knuth Bendix ordering
• Ordinals and Knuth-Bendix orders
• Things to know when implementing KBO
• Automated Deduction – CADE-20

Cites work

• Automating the Knuth Bendix ordering
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 2090305 (Why is no real title available?)
• scientific article; zbMATH DE number 846844 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Modular proof systems for partial functions with Evans equality
• Recursive Path Orderings Can Also Be Incremental
• Refutational theorem proving for hierarchic first-order theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superposition for bounded domains
• Things to know when implementing KBO

Cited in

(25)

• Towards a unified ordering for superposition-based automated reasoning
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• Neural precedence recommender
• A Knuth-Bendix-like ordering for orienting combinator equations
• Set of support, demodulation, paramodulation: a historical perspective
• Model completeness, covers and superposition
• Interpolation systems for ground proofs in automated deduction: a survey
• scientific article; zbMATH DE number 4041334 (Why is no real title available?)
• AC-KBO revisited
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Interpolation and Symbol Elimination
• On transfinite Knuth-Bendix orders
• MetiTarski: An Automatic Prover for the Elementary Functions
• Interpolation and symbol elimination in Vampire
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Superposition for higher-order logic
• Recurrence-Driven Summations in Automated Deduction
• Linear termination is undecidable
• A Formalization of Knuth–Bendix Orders
• A Formalization of Weighted Path Orders and Recursive Path Orders
• Things to know when implementing KBO
• MetiTarski: An automatic theorem prover for real-valued special functions

Describes a project that uses

Uses Software

• SPASS+T
• SPASS
• VAMPIRE

This page was built for publication: An Extension of the Knuth-Bendix Ordering with LPO-Like Properties

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