leanCoP
From MaRDI portal
LeanCoP
Cited in
(76)- Herbrand constructivization for automated intuitionistic theorem proving
- 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
- HOL Based First-Order Modal Logic Provers
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Automated constructivization of proofs
- Automated Reasoning with Analytic Tableaux and Related Methods
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Implementing and evaluating provers for first-order modal logics
- A connection calculus for the description logic \( {\mathcal{ALC}} \)
- Internal guidance for Satallax
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- 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
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Machine learning guidance for connection tableaux
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Monte Carlo tableau proof search
- 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
- scientific article; zbMATH DE number 1765708 (Why is no real title available?)
- Craig interpolation with clausal first-order tableaux
- Efficient Low-Level Connection Tableaux
- Restricting backtracking in connection calculi
- PyRes
- Specifying and verifying organizational security properties in first-order logic
- 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
- MaLeCoP. Machine learning connection prover
- ProofWatch: watchlist guidance for large theories in E
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- BanditFuzz
- HOList
- MleanCoP: a connection prover for first-order modal logic
- Prolog Technology Reinforcement Learning Prover
- nanoCoP: a non-clausal connection prover
- Hammering towards QED
This page was built for software: leanCoP
