IeanCOP: lean connection-based theorem proving
From MaRDI portal
Publication:1404981
DOI10.1016/S0747-7171(03)00037-3zbMath1025.68076MaRDI QIDQ1404981
Publication date: 25 August 2003
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (22)
ENIGMA: efficient learning-based inference guiding machine ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Towards finding longer proofs ⋮ The role of entropy in guiding a connection prover ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Learning theorem proving components ⋮ Efficient Low-Level Connection Tableaux ⋮ Liberalized variable splitting ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ CoProver: a recommender system for proof construction ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ A Non-clausal Connection Calculus ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Proof Search for the First-Order Connection Calculus in Maude ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Automated verification of refinement laws ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ Theorem proving as constraint solving with coherent logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Seventy-five problems for testing automatic theorem provers
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- SETHEO: A high-performance theorem prover
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- The TPTP problem library. CNF release v1. 2. 1
- Controlled integration of the cut rule into connection tableau calculi
- Untersuchungen über das logische Schliessen. I
- lean\(T^ AP\): Lean tableau-based deduction
- Matings in matrices
- Free variable tableaux for propositional modal logics
- ileanTAP: An intuitionistic theorem prover
- T-string unification: Unifying prefixes in non-classical proof methods
- Model elimination without contrapositives
- KoMeT
- Mechanical Theorem-Proving by Model Elimination
This page was built for publication: IeanCOP: lean connection-based theorem proving
