Publication | Date of Publication | Type |
---|
Alien coding | 2023-11-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q5875448 | 2023-02-03 | Paper |
Guiding an automated theorem prover with neural rewriting | 2022-12-07 | Paper |
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) | 2022-11-09 | Paper |
Prolog Technology Reinforcement Learning Prover | 2022-11-09 | Paper |
Towards finding longer proofs | 2022-05-25 | Paper |
The role of entropy in guiding a connection prover | 2022-05-25 | Paper |
Learning theorem proving components | 2022-05-25 | Paper |
Online machine learning techniques for Coq: a comparison | 2022-04-22 | Paper |
Learning to solve geometric construction problems from images | 2022-04-22 | Paper |
Fast and slow enigmas and parental guidance | 2022-03-24 | Paper |
https://portal.mardi4nfdi.de/entity/Q4999300 | 2021-07-06 | Paper |
TacticToe: learning to prove with tactics | 2021-06-09 | Paper |
Machine learning guidance for connection tableaux | 2021-06-09 | Paper |
The Tactician. A seamless, interactive tactic learner and prover for Coq | 2021-01-20 | Paper |
Guiding inferences in connection tableau by recurrent neural networks | 2021-01-20 | Paper |
First neural conjecturing datasets and experiments | 2021-01-20 | Paper |
Hierarchical invention of theorem proving strategies | 2021-01-20 | Paper |
ENIGMAWatch: ProofWatch meets ENIGMA | 2020-05-14 | Paper |
GRUNGE: a grand unified ATP challenge | 2020-03-10 | Paper |
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) | 2020-03-10 | Paper |
Hammering towards QED | 2019-09-18 | Paper |
TacticToe: Learning to Reason with HOL4 Tactics | 2019-01-10 | Paper |
System description: XSL-based translator of Mizar to {\LaTeX} | 2018-10-18 | Paper |
Enhancing ENIGMA given clause guidance | 2018-10-18 | Paper |
First experiments with neural translation of informal to formal mathematics | 2018-10-18 | Paper |
ATPboost: learning premise selection in binary setting with ATP feedback | 2018-10-18 | Paper |
ProofWatch: watchlist guidance for large theories in E | 2018-10-04 | Paper |
Automating formalization by statistical and semantic parsing of mathematics | 2018-01-04 | Paper |
The CADE-25 Automated Theorem Proving system competition – CASC-25 | 2017-11-10 | Paper |
Detecting inconsistencies in large first-order knowledge bases | 2017-09-22 | Paper |
Monte Carlo tableau proof search | 2017-09-22 | Paper |
ENIGMA: efficient learning-based inference guiding machine | 2017-07-21 | Paper |
https://portal.mardi4nfdi.de/entity/Q2988060 | 2017-05-18 | Paper |
Lemmatization for Stronger Reasoning in Large Theories | 2017-02-27 | Paper |
A learning-based fact selector for Isabelle/HOL | 2016-10-27 | Paper |
Extracting Higher-Order Goals from the Mizar Mathematical Library | 2016-08-30 | Paper |
Extending E Prover with Similarity Based Clause Selection Strategies | 2016-08-30 | Paper |
MaLeS: a framework for automatic tuning of automated theorem provers | 2016-05-26 | Paper |
MizAR 40 for Mizar 40 | 2016-05-26 | Paper |
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover | 2016-01-12 | Paper |
System Description: E.T. 0.1 | 2015-12-02 | Paper |
Mizar: State-of-the-art and Beyond | 2015-11-20 | Paper |
Formalizing Physics: Automation, Presentation and Foundation Issues | 2015-11-20 | Paper |
Learning to Parse on Aligned Corpora (Rough Diamond) | 2015-09-14 | Paper |
Premise selection for mathematics by corpus analysis and kernel methods | 2015-07-02 | Paper |
Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) | 2015-07-02 | Paper |
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) | 2015-06-23 | Paper |
HOL(y)Hammer: online ATP service for HOL Light | 2015-03-25 | Paper |
Learning-assisted theorem proving with millions of lemmas | 2015-01-14 | Paper |
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description | 2014-08-07 | Paper |
Lemma Mining over HOL Light | 2014-01-17 | Paper |
Presenting and Explaining Mizar | 2013-12-20 | Paper |
Automated Reasoning Service for HOL Light | 2013-08-09 | Paper |
Formal Mathematics on Display: A Wiki for Flyspeck | 2013-08-09 | Paper |
MaSh: Machine Learning for Sledgehammer | 2013-08-07 | Paper |
Communicating Formal Proofs: The Case of Flyspeck | 2013-08-07 | Paper |
PRocH: Proof Reconstruction for HOL Light | 2013-06-14 | Paper |
E-MaLeS 1.1 | 2013-06-14 | Paper |
MPTP 0.1 - System Description | 2013-04-19 | Paper |
ATP and presentation service for Mizar formalizations | 2013-04-17 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications | 2013-04-17 | Paper |
Theorem Proving in Large Formal Mathematics as an Emerging AI Field | 2013-04-16 | Paper |
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar | 2012-09-07 | Paper |
Point-and-Write – Documenting Formal Mathematics by Reference | 2012-09-07 | Paper |
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics | 2012-09-05 | Paper |
Automated and Human Proofs in General Mathematics: An Initial Comparison | 2012-06-15 | Paper |
Large Formal Wikis: Issues and Solutions | 2011-07-29 | Paper |
Licensing the Mizar Mathematical Library | 2011-07-29 | Paper |
Learning2Reason | 2011-07-29 | Paper |
Automated Proof Compression by Invention of New Definitions | 2011-01-07 | Paper |
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library | 2010-09-14 | Paper |
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar | 2010-08-24 | Paper |
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype | 2010-08-24 | Paper |
ATP-based cross-verification of Mizar proofs: method, systems, and first experiments | 2009-09-18 | Paper |
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance | 2008-11-27 | Paper |
ATP Cross-Verification of the Mizar MPTP Challenge Problems | 2008-05-15 | Paper |
MPTP 0.2: Design, implementation, and initial experiments | 2007-05-03 | Paper |
MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics | 2007-02-20 | Paper |
Mathematical Knowledge Management | 2007-02-12 | Paper |
Mathematical Knowledge Management | 2005-08-26 | Paper |
MPTP-motivation, implementation, first experiments | 2005-06-22 | Paper |
https://portal.mardi4nfdi.de/entity/Q4413895 | 2003-07-21 | Paper |