HOL(y)Hammer: online ATP service for HOL Light (Q2018657): Difference between revisions

@@ Property / cites work @@
+MetiTarski: An automatic theorem prover for real-valued special functions
+Normal rank
@@ Property / cites work @@
+Large Formal Wikis: Issues and Solutions
@@ Property / cites work: Large Formal Wikis: Issues and Solutions / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Encoding Monomorphic and Polymorphic Types
@@ Property / cites work: Encoding Monomorphic and Polymorphic Types / rank @@
+Normal rank
@@ Property / cites work @@
+TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
+Normal rank
@@ Property / cites work @@
+Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
+Normal rank
@@ Property / cites work @@
+Optimizing proof search in model elimination
@@ Property / cites work: Optimizing proof search in model elimination / rank @@
+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 @@
+Web Interfaces for Proof Assistants
@@ Property / cites work: Web Interfaces for Proof Assistants / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning Service for HOL Light
@@ Property / cites work: Automated Reasoning Service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Lemma Mining over HOL Light
@@ Property / cites work: Lemma Mining over 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 @@
+PRocH: Proof Reconstruction for HOL Light
@@ Property / cites work: PRocH: Proof Reconstruction for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Source-Level Proof Reconstruction for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Using the TPTP Language for Writing Derivations and Finite Interpretations
+Normal rank
@@ Property / cites work @@
+Formal Mathematics on Display: A Wiki for Flyspeck
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank