swMATH9756MaRDI QIDQ21735FDOQ21735
Author name not available (Why is that?)
Official website: http://www.leancop.de/
Cited In (75)
- 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 Reasoning with Analytic Tableaux and Related Methods
- Automated constructivization of proofs
- 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
- 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
- ILTP
- Title not available (Why is that?)
- 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
- Craig interpolation with clausal first-order tableaux
- Efficient Low-Level Connection Tableaux
- PyRes
- Restricting backtracking in connection calculi
- Specifying and verifying organizational security properties in first-order logic
- Practical Proof Search for Coq by Type Inhabitation
- BanditFuzz
- HOList
- A Non-clausal Connection Calculus
- Theorem proving as constraint solving with coherent logic
- MaLeCoP. Machine learning connection prover
- A proof-search procedure for intuitionistic propositional logic
- Prolog Technology Reinforcement Learning Prover
- ProofWatch: watchlist guidance for large theories in E
- Hammering towards QED
- MleanCoP: a connection prover for first-order modal logic
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- nanoCoP: a non-clausal connection prover
This page was built for software: leanCoP
