leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
From MaRDI portal
Publication:3541708
DOI10.1007/978-3-540-71070-7_23zbMath1165.68467OpenAlexW1846589774MaRDI QIDQ3541708
Publication date: 27 November 2008
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_23
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
Practical Proof Search for Coq by Type Inhabitation ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ Prolog Technology Reinforcement Learning Prover ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The role of entropy in guiding a connection prover ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Eliminating models during model elimination ⋮ History and Prospects for First-Order Automated Deduction ⋮ A proof-search procedure for intuitionistic propositional logic ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Automated Constructivization of Proofs ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ Internal Guidance for Satallax ⋮ leanCoP ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ Bayesian ranking for strategy scheduling in automated theorem provers ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MPTP 0.2: Design, implementation, and initial experiments
- The ILTP problem library for intuitionistic logic
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- SETHEO: A high-performance theorem prover
- The TPTP problem library. CNF release v1. 2. 1
- Controlled integration of the cut rule into connection tableau calculi
- IeanCOP: lean connection-based theorem proving
- Restricting backtracking in connection calculi
- Matings in matrices
- ileanTAP: An intuitionistic theorem prover
- T-string unification: Unifying prefixes in non-classical proof methods
- A resolution theorem prover for intuitionistic logic
- KoMeT
- LeanT A P: Lean tableau-based theorem proving
- An Intuitionistic Predicate Logic Theorem Prover
- Automated Reasoning with Analytic Tableaux and Related Methods
- Mechanical Theorem-Proving by Model Elimination
This page was built for publication: leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)