Daniel Kuehlwein

I am a PhD student at the Institute for Computing and Information Sciences (ICIS)
Machine Learning and Fountations Group, Faculty of Science
Radboud University Nijmegen

I am working on using machine learning methods to improve automatic theorem proving. One topic is premise selection in automated reasoning in large mathematical domains. MaSh brings the fruits of this research to the users of the Isabelle interactive theorem prover. I also developed MaLeS, an automatic tuning framework for automatic theorem provers. MaLeS combines random-hill climbing based strategy finding with strategy scheduling via learned runtime predictions. For my diplom thesis, I co-developed the Naproche System.

Publications

My PhD thesis Machine Learning for Automated Reasoning can be found here.
A list of my published publications is available at Google Scholar.

Software

MaLeS 1.2
MaLeS is a framework for automatic tuning of automatic theorem provers. E-MaLeS 1.2 and Satallax-MaLeS 1.2 are based upon it. MaLeS supports FOF and THF provers. It finds good strategies and creates strategy schedules based on the features of the problem. The code is hosted at google code. E-MaLeS 1.2 and Satallax-MaLeS 1.2 are also hosted there.
E-MaLeS
E-MaLeS 1.1 is an automatic theorem prover which is based on E prover. E-MaleS uses E with different strategies than the standard auto mode. Furthermore it employs strategy splitting, e.g. it runs several strategies. Note that this version is trained on TPTP problems. You can download the code here.
Multi-Output Ranker (Code used in "Multi-Output Ranking for Automated Reasoning")
Contains the code and the data used in the experiments of the paper "Multi-Output Ranking for Automated Reasoning" You can download the code here.

CASC Results

CASC 24: 1st place in the THF division with Satallax-MaLeS 1.2. 4th place in the FOF division with E-MaLeS 1.2.
CASC J6: 2nd place in the FOF division with E-MaLeS 1.1.
CASC@Turing: 2nd place in the FOF division with E-MaLeS 1.1. 3rd place in the MZR@Turing division with PS-E.
CASC 23: 3rd place in the FOF division with E-MaLeS 1.0.

E-MaLeS and PS-E are based on the E prover by Stephan Schulz. Satallex-MaLeS uses Satallax by Chad Brown.

Contact information

Email

kuehlwein[at]science.ru.nl

Phone

+31-24-3652172

Postal Address

Faculty of Science
University of Nijmegen
Postbus 9010
6500 GL Nijmegen
The Netherlands

Visiting Address

Room HG02.540
Faculty of Science
Heijendaalseweg 135
6525 AJ Nijmegen