Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
From MaRDI portal
Publication:2351415
DOI10.1007/s10817-014-9303-3zbMath1314.68283arXiv1211.7012OpenAlexW2156433885WikidataQ59321365 ScholiaQ59321365MaRDI QIDQ2351415
Publication date: 23 June 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1211.7012
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE, Finding proofs in Tarskian geometry, ENIGMA: efficient learning-based inference guiding machine, Improving stateful premise selection with transformers, MizAR 40 for Mizar 40, The higher-order prover \textsc{Leo}-II, Semi-intelligible Isar proofs from machine-generated proofs, JEFL: joint embedding of formal proof libraries, ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Formalizing Physics: Automation, Presentation and Foundation Issues, Automated Reasoning in the Wild, On the formal analysis of Gaussian optical systems in HOL, Aligning concepts across proof assistant libraries, A learning-based fact selector for Isabelle/HOL, Hammer for Coq: automation for dependent type theory, Automating formalization by statistical and semantic parsing of mathematics, Machine Learning for Inductive Theorem Proving, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Random Forests for Premise Selection, Lemmatization for Stronger Reasoning in Large Theories, Learning-assisted theorem proving with millions of lemmas, Hammering Mizar by Learning Clause Guidance (Short Paper)., HOL(y)Hammer: online ATP service for HOL Light, TacticToe: learning to prove with tactics, Machine learning guidance for connection tableaux, Internal Guidance for Satallax, GRUNGE: a grand unified ATP challenge, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), Matching Concepts across HOL Libraries, Mining State-Based Models from Proof Corpora, Towards Knowledge Management for HOL Light, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings
- Automated deduction -- CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 -- August 5, 2011. Proceedings
- MPTP-motivation, implementation, first experiments
- Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11--15, 2012. Proceedings
- MPTP 0.2: Design, implementation, and initial experiments
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
- MetiTarski: An automatic theorem prover for real-valued special functions
- A revision of the proof of the Kepler conjecture
- 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
- On computer-assisted proofs in ordinal number theory
- ATP and presentation service for Mizar formalizations
- Premise selection for mathematics by corpus analysis and kernel methods
- Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
- Translating higher-order clauses to first-order clauses
- Web Interfaces for Proof Assistants
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- The TPTP Typed First-Order Form with Arithmetic
- Satallax: An Automatic Higher-Order Prover
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- More SPASS with Isabelle
- MaLeCoP Machine Learning Connection Prover
- Automatic Proof and Disproof in Isabelle/HOL
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- Using the TPTP Language for Writing Derivations and Finite Interpretations
- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
- Optimizing proof search in model elimination
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Extending Sledgehammer with SMT Solvers
- Sine Qua Non for Large Theory Reasoning
- Large Formal Wikis: Issues and Solutions
- Encoding Monomorphic and Polymorphic Types
- Scalable LCF-Style Proof Translation
- Mechanical Theorem-Proving by Model Elimination
- The Principal Type-Scheme of an Object in Combinatory Logic
- Sledgehammer: Judgement Day
- Automatic derivation of the irrationality of \(e\)
