Ordered chaining for total orderings

DOI10.1007/3-540-58156-1_32zbMath1433.68528OpenAlexW1544409518MaRDI QIDQ5210789

Harald Ganzinger, Leo Bachmair

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-0014-B49B-C

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Total orders (06A05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Cancellative Abelian monoids and related structures in refutational theorem proving. II

Cites Work

• Simple LPO constraint solving methods
• Challenge problems in elementary calculus
• Completeness results for inequality provers
• Completeness of a prover for dense linear orders
• Ordered chaining calculi for first-order theories of transitive relations
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Bi-rewriting, a term rewriting technique for monotonic order relations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item