Connection tableaux with lazy paramodulation

DOI10.1007/S10817-007-9089-7zbMath1144.03008OpenAlexW2045057655MaRDI QIDQ928656

Andrei Paskevich

Publication date: 11 June 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-007-9089-7

zbMATH Keywords

first-order logic with equalitybasic ordered paramodulationconnection tableauxlazy paramodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (3)

\textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ Building Theorem Provers ⋮ The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• SETHEO
• E-SETHEO

Cites Work

• SETHEO: A high-performance theorem prover
• Complete sets of transformations for general E-unification
• What you always wanted to know about rigid \(E\)-unification
• Basic paramodulation
• Connection Tableaux with Lazy Paramodulation
• Proving Theorems with the Modification Method
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Connection tableaux with lazy paramodulation