leanCoP
From MaRDI portal
LeanCoP
Cited in
(76)- HOL Based First-Order Modal Logic Provers
- Hammering towards QED
- A connection calculus for the description logic \( {\mathcal{ALC}} \)
- Craig interpolation with clausal first-order tableaux
- Internal guidance for Satallax
- 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
- Specifying and verifying organizational security properties in first-order logic
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- MleanCoP: a connection prover for first-order modal logic
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- A Non-clausal Connection Calculus
- Practical Proof Search for Coq by Type Inhabitation
- Machine learning guidance for connection tableaux
- nanoCoP: a non-clausal connection prover
- MaLeCoP. Machine learning connection prover
- Monte Carlo tableau proof search
- Certification of nonclausal connection tableaux proofs
- Restricting backtracking in connection calculi
- Theorem proving as constraint solving with coherent logic
- A proof-search procedure for intuitionistic propositional logic
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ILTP
- SETHEO
- Prover9
- Mace4
- Zenon
- E-SETHEO
- MaLeCoP
- ileanCoP
- DLog
- JProver
- leanTAP
- QMLTP
- ModLeanTAP
- Beagle
- SMTtoTPTP
- FOOL
- randoCoP
- FEMaLeCoP
- IDV
- MleanCoP
- nanoCoP
- SWI-Prolog
- GAPT
- ProofTool
- DeepMath
- ENIGMA
- KoMeT
- Proofwatch
- Holophrasm
- CoDe
- GKC
- DLPEQ
- TreeRePair
- lpeq
- intuit
- Slakje
- WhaleProver
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Efficient Low-Level Connection Tableaux
- PyRes
- Bayesian ranking for strategy scheduling in automated theorem provers
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- Implementing and evaluating provers for first-order modal logics
- BanditFuzz
- HOList
- scientific article; zbMATH DE number 1765708 (Why is no real title available?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- ProofWatch: watchlist guidance for large theories in E
- Prolog Technology Reinforcement Learning Prover
- Automated constructivization of proofs
- Herbrand constructivization for automated intuitionistic theorem proving
This page was built for software: leanCoP
