On Transfinite Knuth-Bendix Orders

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Neural precedence recommender

Uses Software

• MetiTarski
• OTTER
• VAMPIRE
• SPASS
• TPTP
• Waldmeister

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