|
|
(4 intermediate revisions by 4 users not shown) |
Property / DOI | |
| | |
Property / DOI: 10.1007/s10817-020-09576-7 / rank | |
| Normal rank
| |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: ENIGMA / rank |
| | Normal rank |
| Property / MaRDI profile type |
| | |
| Property / MaRDI profile type: MaRDI publication profile / rank |
| | Normal rank |
| Property / full work available at URL |
| | |
| Property / full work available at URL: https://doi.org/10.1007/s10817-020-09576-7 / rank |
| | Normal rank |
| Property / OpenAlex ID |
| | |
| Property / OpenAlex ID: W3083107390 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automated and Human Proofs in General Mathematics: An Initial Comparison / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Premise selection for mathematics by corpus analysis and kernel methods / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: On connections and higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: lean\(T^ AP\): Lean tableau-based deduction / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4282596 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Short Presentation of Coq / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Matings in matrices / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4692618 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4003525 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A vision for automated deduction rooted in the connection method / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Hammering towards QED / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A learning-based fact selector for Isabelle/HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Brief Overview of Agda – A Functional Language with Dependent Types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4--8, 2011. Proceedings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Internal Guidance for Satallax / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Monte Carlo tableau proof search / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Connection methods in linear logic and proof nets construction / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4263014 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2751354 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: HOL Light: An Overview / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5772177 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Game-theoretical semantics: Insights and prospects / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Sine Qua Non for Large Theory Reasoning / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Selecting the Selection / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: ENIGMA: efficient learning-based inference guiding machine / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MizAR 40 for Mizar 40 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: System Description: E.T. 0.1 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MaSh: Machine Learning for Sledgehammer / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2751380 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: SETHEO: A high-performance theorem prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Deep Network Guided Proof Search / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Mechanical Theorem-Proving by Model Elimination / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Lightweight relevance filtering for machine-generated resolution problems / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automated Reasoning with Analytic Tableaux and Related Methods / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Restricting backtracking in connection calculi / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Non-clausal Connection Calculus / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MleanCoP: A Connection Prover for First-Order Modal Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: nanoCoP: A Non-clausal Connection Prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: IeanCOP: lean connection-based theorem proving / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A structure-preserving clause form translation / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2751378 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The ILTP problem library for intuitionistic logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2724150 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4797437 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: System Description: E 1.8 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Brief Overview of HOL4 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The 8th IJCAR automated theorem proving system competition – CASC-J8 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The CADE-14 ATP system competition / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MPTP-motivation, implementation, first experiments / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Evaluation of Automated Theorem Proving on the Mizar Mathematical Library / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MaLeCoP Machine Learning Connection Prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Using hints to increase the effectiveness of an automated reasoning program: Case studies / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The Isabelle Framework / rank |
| | Normal rank |
| Property / DOI |
| | |
| Property / DOI: 10.1007/S10817-020-09576-7 / rank |
| | Normal rank |