research
∙
03/12/2023
MizAR 60 for Mizar 50
As a present to Mizar on its 50th anniversary, we develop an AI/TP syste...
share
research
∙
05/04/2022
The Isabelle ENIGMA
We significantly improve the performance of the E automated theorem prov...
research
∙
07/21/2021
Learning Theorem Proving Components
Saturation-style automated theorem provers (ATPs) based on the given cla...
research
∙
07/14/2021
Fast and Slow Enigmas and Parental Guidance
We describe several additions to the ENIGMA system that guides clause se...
research
∙
05/29/2020
First Neural Conjecturing Datasets and Experiments
We describe several datasets and first experiments with creating conject...
research
∙
02/13/2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
We describe an implementation of gradient boosting and neural guidance o...
research
∙
05/23/2019
ENIGMAWatch: ProofWatch Meets ENIGMA
In this work we describe a new learning-based proof guidance -- ENIGMAWa...
research
∙
04/02/2019
Hammering Mizar by Learning Clause Guidance
We describe a very large improvement of existing hammer-style proof auto...
research
∙
03/07/2019
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
We describe an efficient implementation of clause guidance in saturation...
research
∙
02/12/2018
ProofWatch: Watchlist Guidance for Large Theories in E
Watchlist (also hint list) is a mechanism that allows related proofs to ...
research
∙
01/23/2017
ENIGMA: Efficient Learning-based Inference Guiding Machine
ENIGMA is a learning-based method for guiding given clause selection in ...
research
∙
11/26/2016