Connection tableaux with lazy paramodulation

DOI10.1007/S10817-007-9089-7MaRDI QIDQ928656zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Connection Tableaux with Lazy Paramodulation
• scientific article; zbMATH DE number 2219496
• The disconnection tableau calculus
• Hyper Tableaux with Equality
• The hyper tableaux calculus with equality and an application to finite model computation

Cites work

• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1303344 (Why is no real title available?)
• scientific article; zbMATH DE number 1950258 (Why is no real title available?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Basic paramodulation
• Complete sets of transformations for general E-unification
• Connection Tableaux with Lazy Paramodulation
• Model elimination and connection tableau procedures
• Paramodulation-based theorem proving
• Proving Theorems with the Modification Method
• SETHEO: A high-performance theorem prover
• What you always wanted to know about rigid \(E\)-unification

Cited in

(8)

• Building Theorem Provers
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• scientific article; zbMATH DE number 834568 (Why is no real title available?)
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• Connection Tableaux with Lazy Paramodulation
• Efficient Low-Level Connection Tableaux
• First-order tableaux in applications (extended abstract)
• scientific article; zbMATH DE number 1882047 (Why is no real title available?)

Describes a project that uses

Uses Software

• SETHEO
• E-SETHEO

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q928656)