IeanCOP: lean connection-based theorem proving
From MaRDI portal
Recommendations
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Publication:4539650
- Automated Reasoning with Analytic Tableaux and Related Methods
- MleanCoP: a connection prover for first-order modal logic
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
Cites work
- scientific article; zbMATH DE number 1612568 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 4110158 (Why is no real title available?)
- scientific article; zbMATH DE number 3731310 (Why is no real title available?)
- scientific article; zbMATH DE number 1341478 (Why is no real title available?)
- scientific article; zbMATH DE number 1543301 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Controlled integration of the cut rule into connection tableau calculi
- Free variable tableaux for propositional modal logics
- Implementing semantic tableaux
- Matings in matrices
- Mechanical Theorem-Proving by Model Elimination
- Model elimination without contrapositives
- SETHEO: A high-performance theorem prover
- Seventy-five problems for testing automatic theorem provers
- T-string unification: unifying prefixes in non-classical proof methods
- The TPTP problem library. CNF release v1. 2. 1
- Untersuchungen über das logische Schliessen. I
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- lean\(T^ AP\): Lean tableau-based deduction
Cited in
(35)- Learning theorem proving components
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- The role of entropy in guiding a connection prover
- ENIGMA: efficient learning-based inference guiding machine
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- Towards finding longer proofs
- Specifying and verifying organizational security properties in first-order logic
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- MleanCoP: a connection prover for first-order modal logic
- A Non-clausal Connection Calculus
- scientific article; zbMATH DE number 1765687 (Why is no real title available?)
- Proof Search for the First-Order Connection Calculus in Maude
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Machine learning guidance for connection tableaux
- nanoCoP: a non-clausal connection prover
- Theorem proving in large formal mathematics as an emerging AI field
- MaLeCoP. Machine learning connection prover
- Restricting backtracking in connection calculi
- Liberalized variable splitting
- Theorem proving as constraint solving with coherent logic
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
- Lemmas: generation, selection, application
- Range-restricted and Horn interpolation through clausal tableaux
- Efficient Low-Level Connection Tableaux
- From Schütte’s Formal Systems to Modern Automated Deduction
- Voting theory in the Lean theorem prover
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- lean\(T^ AP\): Lean tableau-based deduction
- scientific article; zbMATH DE number 1765708 (Why is no real title available?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- CoProver: a recommender system for proof construction
- Prolog Technology Reinforcement Learning Prover
- Automated verification of refinement laws
This page was built for publication: IeanCOP: lean connection-based theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1404981)
