leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)

DOI10.1007/978-3-540-71070-7_23zbMath1165.68467OpenAlexW1846589774MaRDI QIDQ3541708

Jens Otten

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

Mathematics Subject Classification ID

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

• SETHEO
• OTTER
• TPTP
• ileanCoP
• JProver

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)