Machine learning guidance for connection tableaux (Q2031418): Difference between revisions

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