On using ground joinable equations in equational theorem proving

DOI10.1016/S0747-7171(03)00024-5zbMath1019.03005MaRDI QIDQ1404987

Th. Hillenbrand, Jürgen Avenhaus, Bernd Löchner

Publication date: 25 August 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

completionrewritingequational theorem provingground joinable equations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Implementing Superposition in iProver (System Description) ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Citius altius fortius ⋮ Twee: an equational theorem prover ⋮ Certified equational reasoning via ordered completion ⋮ Extending Maximal Completion (Invited Talk) ⋮ Ground joinability and connectedness in the superposition calculus

Uses Software

• TPTP
• Waldmeister

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Towards a foundation of completion procedures as semidecision procedures
• On ground-confluence of term rewriting systems
• The TPTP problem library. CNF release v1. 2. 1
• Theorem proving with ordering and equality constrained clauses
• The CADE-16 ATP system competition
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Complete Sets of Reductions for Some Equational Theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification