leanCoP

swMATH9756MaRDI QIDQ21735

No author found.

Described by source

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

Related Items (36)

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 ⋮ Efficient Low-Level Connection Tableaux ⋮ FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover ⋮ MleanCoP: A Connection Prover for First-Order Modal Logic ⋮ Unnamed Item ⋮ Monte Carlo tableau proof search ⋮ A proof-search procedure for intuitionistic propositional logic ⋮ Craig interpolation with clausal first-order tableaux ⋮ Certification of nonclausal connection tableaux proofs ⋮ Herbrand constructivization for automated intuitionistic theorem proving ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Automated Constructivization of Proofs ⋮ A Non-clausal Connection Calculus ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Restricting backtracking in connection calculi ⋮ Unnamed Item ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ ProofWatch: watchlist guidance for large theories in E ⋮ Unnamed Item ⋮ A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$ ⋮ Automated Reasoning with Analytic Tableaux and Related Methods ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ Internal Guidance for Satallax ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Theorem proving as constraint solving with coherent logic ⋮ Bayesian ranking for strategy scheduling in automated theorem provers ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ Hammering towards QED ⋮ HOL Based First-Order Modal Logic Provers

This page was built for software: leanCoP