Restricting backtracking in connection calculi
From MaRDI portal
Recommendations
Cited in
(23)- Machine learning guidance for connection tableaux
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- Eliminating models during model elimination
- Craig interpolation with clausal first-order tableaux
- A connection calculus for the description logic \( {\mathcal{ALC}} \)
- nanoCoP: a non-clausal connection prover
- A Non-clausal Connection Calculus
- MaLeCoP. Machine learning connection prover
- Specifying and verifying organizational security properties in first-order logic
- Efficient Low-Level Connection Tableaux
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- scientific article; zbMATH DE number 1341619 (Why is no real title available?)
- scientific article; zbMATH DE number 517070 (Why is no real title available?)
- From Schütte’s Formal Systems to Modern Automated Deduction
- Cardinality Restrictions Within Description Logic Connection Calculi
- On structures of regular standard contradictions in propositional logic
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Range-restricted and Horn interpolation through clausal tableaux
- Lemmas: generation, selection, application
- Investigations into proof structures
- Constraint learning for non-confluent proof search
- Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic
This page was built for publication: Restricting backtracking in connection calculi
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3568228)
