Connection tableaux with lazy paramodulation

DOI10.1007/S10817-007-9089-7zbMATH Open1144.03008OpenAlexW2045057655MaRDI QIDQ928656FDOQ928656

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

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

zbMATH Keywords

first-order logic with equalitybasic ordered paramodulationconnection tableauxlazy paramodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• SETHEO: A high-performance theorem prover
• Model elimination and connection tableau procedures
• Title not available (Why is that?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Basic paramodulation
• Paramodulation-based theorem proving
• What you always wanted to know about rigid \(E\)-unification
• Complete sets of transformations for general E-unification
• Proving Theorems with the Modification Method
• Title not available (Why is that?)
• Connection Tableaux with Lazy Paramodulation
• Title not available (Why is that?)

Cited In (8)

• Building Theorem Provers
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• Title not available (Why is that?)
• Connection Tableaux with Lazy Paramodulation
• Title not available (Why is that?)
• First-order tableaux in applications (extended abstract)
• Efficient Low-Level Connection Tableaux
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search

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)