On Transfinite Knuth-Bendix Orders
From MaRDI portal
Publication:5200038
DOI10.1007/978-3-642-22438-6_29zbMath1341.68194OpenAlexW69093803MaRDI QIDQ5200038
Laura Kovács, Andrei Voronkov, Georg Moser
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_29
Related Items
Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Neural precedence recommender
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The Hydra battle and Cichon's principle
- KBO orientability
- Things to know when implementing KBO
- MetiTarski: An automatic theorem prover for real-valued special functions
- Orienting rewrite rules with the Knuth-Bendix order.
- The CADE-16 ATP system competition
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- System Description: Spass Version 3.0
- Accessible Independence Results for Peano Arithmetic
- Term Rewriting and All That
- Interpolation and Symbol Elimination
- Automated Reasoning