Constraint learning for non-confluent proof search
From MaRDI portal
Cites work
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- Backjumping is Exception Handling
- Connection tableaux with lazy paramodulation
- Efficient Low-Level Connection Tableaux
- Eliminating models during model elimination
- Encoding First Order Proofs in SAT
- scientific article; zbMATH DE number 1189104 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- Investigations into proof structures
- IPASIR-up: user propagators for CDCL
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Mechanical Theorem-Proving by Model Elimination
- MleanCoP: a connection prover for first-order modal logic
- Model elimination and connection tableau procedures
- nanoCoP: a non-clausal connection prover
- Paramodulation-based theorem proving
- Premise selection for mathematics by corpus analysis and kernel methods
- Prolog Technology Reinforcement Learning Prover
- Proving Theorems with the Modification Method
- Restricting backtracking in connection calculi
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Theorem Proving via General Matings
- Theorem proving with bounded rigid E-unification
- Translating higher-order clauses to first-order clauses
This page was built for publication: Constraint learning for non-confluent proof search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860392)
