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