leanCoP

swMATH9756MaRDI QIDQ21735FDOQ21735

Author name not available (Why is that?)

Described by source

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

Cited In (36)

• Herbrand constructivization for automated intuitionistic theorem proving
• Specifying and Verifying Organizational Security Properties in First-Order Logic
• Bayesian ranking for strategy scheduling in automated theorem provers
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Certification of nonclausal connection tableaux proofs
• MaLeCoP Machine Learning Connection Prover
• nanoCoP: A Non-clausal Connection Prover
• HOL Based First-Order Modal Logic Provers
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• MleanCoP: A Connection Prover for First-Order Modal Logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• Title not available (Why is that?)
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Eliminating models during model elimination
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• The role of entropy in guiding a connection prover
• Machine learning guidance for connection tableaux
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Monte Carlo tableau proof search
• Title not available (Why is that?)
• Automated Constructivization of Proofs
• A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$
• Internal Guidance for Satallax
• Craig interpolation with clausal first-order tableaux
• Efficient Low-Level Connection Tableaux
• Restricting backtracking in connection calculi
• Practical Proof Search for Coq by Type Inhabitation
• A Non-clausal Connection Calculus
• Theorem proving as constraint solving with coherent logic
• A proof-search procedure for intuitionistic propositional logic
• Prolog Technology Reinforcement Learning Prover
• ProofWatch: watchlist guidance for large theories in E
• Hammering towards QED
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• Title not available (Why is that?)

This page was built for software: leanCoP