MleanCoP: a connection prover for first-order modal logic
From MaRDI portal
Publication:3192198
DOI10.1007/978-3-319-08587-6_20zbMATH Open1423.68423OpenAlexW102946451MaRDI QIDQ3192198FDOQ3192198
Recommendations
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Implementing and evaluating provers for first-order modal logics
- First-order modal tableaux
- IeanCOP: lean connection-based theorem proving
- Implementing a relational theorem prover for modal logic K
Cited In (19)
- Solving modal logic problems by translation to higher-order logic
- Local reductions for the modal cube
- From Schütte’s Formal Systems to Modern Automated Deduction
- Extensional higher-order paramodulation in Leo-III
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Implementing and evaluating provers for first-order modal logics
- Eliminating models during model elimination
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- Machine learning guidance for connection tableaux
- IeanCOP: lean connection-based theorem proving
- MleanCoP
- Higher-order modal logics: automation and applications
- Efficient local reductions to basic modal logic
- Title not available (Why is no real title available?)
- Proof Search for the First-Order Connection Calculus in Maude
- Local is best: efficient reductions to modal logic \textsf{K}
- Prolog Technology Reinforcement Learning Prover
- nanoCoP: a non-clausal connection prover
Uses Software
This page was built for publication: MleanCoP: a connection prover for first-order modal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192198)
