An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
From MaRDI portal
Publication:3498479
DOI10.1007/978-3-540-75560-9_26zbMath1137.03306OpenAlexW1584399668MaRDI QIDQ3498479
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
Related Items (17)
Interpolation systems for ground proofs in automated deduction: a survey ⋮ AC-KBO revisited ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Superposition for higher-order logic ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Interpolation and Symbol Elimination ⋮ On Transfinite Knuth-Bendix Orders ⋮ Unnamed Item ⋮ 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 ⋮ Model completeness, covers and superposition ⋮ MetiTarski: An Automatic Prover for the Elementary Functions ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automating the Knuth Bendix ordering
- Things to know when implementing KBO
- Refutational theorem proving for hierarchic first-order theories
- Modular proof systems for partial functions with Evans equality
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Superposition for Bounded Domains
- Recursive Path Orderings Can Also Be Incremental
This page was built for publication: An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
