Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415): Difference between revisions

@@ Property / Wikidata QID @@
+Q59321365
@@ Property / Wikidata QID: Q59321365 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MetiTarski
@@ Property / describes a project that uses: MetiTarski / 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 @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / 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 @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Prover9
@@ Property / describes a project that uses: Prover9 / 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 @@
+Satallax
@@ Property / describes a project that uses: Satallax / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mace4
@@ Property / describes a project that uses: Mace4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BliStr
@@ Property / describes a project that uses: BliStr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Zero
@@ Property / describes a project that uses: HOL Zero / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+miz3
@@ Property / describes a project that uses: miz3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TRAMP
@@ Property / describes a project that uses: TRAMP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Caduceus
@@ Property / describes a project that uses: Caduceus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PERL
@@ Property / describes a project that uses: PERL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MPTP 0.2
@@ Property / describes a project that uses: MPTP 0.2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+KRAKATOA
@@ Property / describes a project that uses: KRAKATOA / 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 @@
+SPASS+T
@@ Property / describes a project that uses: SPASS+T / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MoMM
@@ Property / describes a project that uses: MoMM / 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 @@
+Ivy
@@ Property / describes a project that uses: Ivy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEO-II
@@ Property / describes a project that uses: LEO-II / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OTTER
@@ Property / describes a project that uses: OTTER / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Why3
@@ Property / describes a project that uses: Why3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / 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 @@
+Gandalf
@@ Property / describes a project that uses: Gandalf / 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 @@
+MaLARea
@@ Property / describes a project that uses: MaLARea / 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 @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2156433885
@@ Property / OpenAlex ID: W2156433885 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.7012
@@ Property / arXiv ID: 1211.7012 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075241
@@ Property / cites work: Q3075241 / rank @@
+Normal rank
@@ 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 @@
+Automated and Human Proofs in General Mathematics: An Initial Comparison
+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 @@
+Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5--10, 2010. Proceedings
+Normal rank
@@ Property / cites work @@
+Automatic derivation of the irrationality of \(e\)
+Normal rank
@@ Property / cites work @@
+On computer-assisted proofs in ordinal number theory
+Normal rank
@@ Property / cites work @@
+LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+Automated deduction -- CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 -- August 5, 2011. Proceedings
+Normal rank
@@ Property / cites work @@
+Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11--15, 2012. Proceedings
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Encoding Monomorphic and Polymorphic Types
@@ Property / cites work: Encoding Monomorphic and Polymorphic Types / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Proof and Disproof in Isabelle/HOL
@@ Property / cites work: Automatic Proof and Disproof in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
+Normal rank
@@ Property / cites work @@
+More SPASS with Isabelle
@@ Property / cites work: More SPASS with Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Satallax: An Automatic Higher-Order Prover
@@ Property / cites work: Satallax: An Automatic Higher-Order Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4503907
@@ Property / cites work: Q4503907 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
+Normal rank
@@ Property / cites work @@
+Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
+Normal rank
@@ Property / cites work @@
+Q4520767
@@ Property / cites work: Q4520767 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings
+Normal rank
@@ Property / cites work @@
+A revision of the proof of the Kepler conjecture
@@ Property / cites work: A revision of the proof of the Kepler conjecture / rank @@
+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 @@
+The Principal Type-Scheme of an Object in Combinatory Logic
+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 @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+Q4809048
@@ Property / cites work: Q4809048 / 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 @@
+Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
+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 @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692514
@@ Property / cites work: Q4692514 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723444
@@ Property / cites work: Q2723444 / rank @@
+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 @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4032144
@@ Property / cites work: Q4032144 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4413892
@@ Property / cites work: Q4413892 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP Typed First-Order Form with Arithmetic
@@ Property / cites work: The TPTP Typed First-Order Form with Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Using the TPTP Language for Writing Derivations and Finite Interpretations
+Normal rank
@@ Property / cites work @@
+Q4413895
@@ Property / cites work: Q4413895 / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+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 @@
+Theorem Proving in Large Formal Mathematics as an Emerging AI Field
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4500649
@@ Property / cites work: Q4500649 / rank @@
+Normal rank
@@ Property / cites work @@
+A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
+Normal rank
@@ Property / DBLP publication ID @@
+journals/jar/KaliszykU14
@@ Property / DBLP publication ID: journals/jar/KaliszykU14 / rank @@
+Normal rank