| Publication | Date of Publication | Type |
|---|
Invariant neural architecture for learning term synthesis in instantiation proving
Journal of Symbolic Computation | 2024-12-09 | Paper |
Solving hard Mizar problems with instantiation and strategy invention
| 2024-12-04 | Paper |
Automated theorem proving for Metamath
| 2024-11-26 | Paper |
Mizar 60 for Mizar 50
| 2024-11-26 | Paper |
Initial experiments with TPTP-style automated theorem provers on ACL2 problems
| 2024-08-19 | Paper |
The Isabelle ENIGMA
| 2024-07-15 | Paper |
Learning Proof Transformations and Its Applications in Interactive Theorem Proving
| 2024-05-03 | Paper |
Translating SUMO-K to Higher-Order Set Theory
| 2024-05-03 | Paper |
Alien coding
International Journal of Approximate Reasoning | 2023-11-16 | Paper |
Hammering Mizar by Learning Clause Guidance (Short Paper).
| 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)
Automated Reasoning | 2022-11-09 | Paper |
Prolog Technology Reinforcement Learning Prover
Automated Reasoning | 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 |
Property invariant embedding for automated reasoning
| 2021-07-06 | Paper |
TacticToe: learning to prove with tactics
Journal of Automated Reasoning | 2021-06-09 | Paper |
Machine learning guidance for connection tableaux
Journal of Automated Reasoning | 2021-06-09 | Paper |
Hierarchical invention of theorem proving strategies
AI Communications | 2021-01-20 | Paper |
The Tactician. A seamless, interactive tactic learner and prover for Coq
| 2021-01-20 | Paper |
First neural conjecturing datasets and experiments
| 2021-01-20 | Paper |
Guiding inferences in connection tableau by recurrent neural networks
| 2021-01-20 | Paper |
ENIGMAWatch: ProofWatch meets ENIGMA
| 2020-05-14 | Paper |
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
| 2020-03-10 | Paper |
GRUNGE: a grand unified ATP challenge
| 2020-03-10 | Paper |
Hammering towards QED
| 2019-09-18 | Paper |
TacticToe: learning to reason with HOL4 tactics
EPiC Series in Computing | 2019-01-10 | Paper |
Enhancing ENIGMA given clause guidance
| 2018-10-18 | Paper |
ATPboost: learning premise selection in binary setting with ATP feedback
| 2018-10-18 | Paper |
System description: XSL-based translator of Mizar to {\LaTeX}
| 2018-10-18 | Paper |
First experiments with neural translation of informal to formal mathematics
| 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
AI Communications | 2017-11-10 | Paper |
Monte Carlo tableau proof search
| 2017-09-22 | Paper |
Detecting inconsistencies in large first-order knowledge bases
| 2017-09-22 | Paper |
ENIGMA: efficient learning-based inference guiding machine
| 2017-07-21 | Paper |
A mathematical proof proved correct: the most efficient way to pack spheres
| 2017-05-18 | Paper |
Lemmatization for stronger reasoning in large theories
Frontiers of Combining Systems | 2017-02-27 | Paper |
A learning-based fact selector for Isabelle/HOL
Journal of Automated Reasoning | 2016-10-27 | Paper |
Extending E prover with similarity based clause selection strategies
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Extracting Higher-Order Goals from the Mizar Mathematical Library
Lecture Notes in Computer Science | 2016-08-30 | Paper |
MizAR 40 for Mizar 40
Journal of Automated Reasoning | 2016-05-26 | Paper |
MaLeS: a framework for automatic tuning of automated theorem provers
Journal of Automated Reasoning | 2016-05-26 | Paper |
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
System description: E.T. 0.1
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Mizar: state-of-the-art and beyond
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Formalizing physics: automation, presentation and foundation issues
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Learning to parse on aligned corpora (rough diamond)
Interactive Theorem Proving | 2015-09-14 | Paper |
Premise selection for mathematics by corpus analysis and kernel methods
Journal of Automated Reasoning | 2015-07-02 | Paper |
Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Journal of Automated Reasoning | 2015-07-02 | Paper |
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Journal of Automated Reasoning | 2015-06-23 | Paper |
HOL(y)Hammer: online ATP service for HOL Light
Mathematics in Computer Science | 2015-03-25 | Paper |
Learning-assisted theorem proving with millions of lemmas
Journal of Symbolic Computation | 2015-01-14 | Paper |
Developing corpus-based translation methods between informal and formal mathematics: project description
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Lemma Mining over HOL Light
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Presenting and explaining Mizar
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Automated reasoning service for HOL Light
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Formal mathematics on display: a wiki for Flyspeck
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Communicating formal proofs: the case of Flyspeck
Interactive Theorem Proving | 2013-08-07 | Paper |
MaSh: machine learning for Sledgehammer
Interactive Theorem Proving | 2013-08-07 | Paper |
PRocH: proof reconstruction for HOL Light
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
E-MaLeS 1.1
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
MPTP 0.1 -- system description
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications
Journal of Automated Reasoning | 2013-04-17 | Paper |
ATP and presentation service for Mizar formalizations
Journal of Automated Reasoning | 2013-04-17 | Paper |
Theorem proving in large formal mathematics as an emerging AI field
Automated Reasoning and Mathematics | 2013-04-16 | Paper |
Dependencies in formal mathematics: applications and extraction for Coq and Mizar
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Point-and-write -- documenting formal mathematics by reference
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Overview and evaluation of premise selection techniques for large theory mathematics
Automated Reasoning | 2012-09-05 | Paper |
Automated and human proofs in general mathematics: an initial comparison
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Licensing the Mizar Mathematical Library (MML)
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Large formal wikis: issues and solutions
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Learning2Reason
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Automated proof compression by invention of new definitions
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Evaluation of automated theorem proving on the Mizar mathematical library
Mathematical Software – ICMS 2010 | 2010-09-14 | Paper |
Automated reasoning and presentation support for formalizing mathematics in MizAR
Lecture Notes in Computer Science | 2010-08-24 | Paper |
A Wiki for Mizar: motivation, considerations, and initial prototype
Lecture Notes in Computer Science | 2010-08-24 | Paper |
ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
Mathematics in Computer Science | 2009-09-18 | Paper |
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
Automated Reasoning | 2008-11-27 | Paper |
ATP Cross-Verification of the Mizar MPTP Challenge Problems
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
MPTP 0.2: Design, implementation, and initial experiments
Journal of Automated Reasoning | 2007-05-03 | Paper |
MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
Journal of Applied Logic | 2007-02-20 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
MPTP-motivation, implementation, first experiments
Journal of Automated Reasoning | 2005-06-22 | Paper |
scientific article; zbMATH DE number 1951640 (Why is no real title available?)
| 2003-07-21 | Paper |
