Recommendations
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?)
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)