
Online Machine Learning Techniques for Coq: A Comparison
We present a comparison of several online machine learning techniques fo...
read it

Disambiguating Symbolic Expressions in Informal Documents
We propose the task of disambiguating symbolic expressions in informal S...
read it

A Study of Continuous Vector Representationsfor Theorem Proving
Applying machine learning to mathematical terms and formulas requires a ...
read it

A Survey of Languages for Formalizing Mathematics
In order to work with mathematical content in computer systems, it is ne...
read it

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
In this paper we share several experiments trying to automatically trans...
read it

Property Invariant Embedding for Automated Reasoning
Automated reasoning and theorem proving have recently become major chall...
read it

Can Neural Networks Learn Symbolic Rewriting?
This work investigates if the current neural architectures are adequate ...
read it

Towards Finding Longer Proofs
We present a reinforcement learning (RL) based guidance system for autom...
read it

GRUNGE: A Grand Unified ATP Challenge
This paper describes a large set of related theorem proving problems obt...
read it

Concrete Semantics with Coq and CoqHammer
The "Concrete Semantics" book gives an introduction to imperative progra...
read it

Reinforcement Learning of Theorem Proving
We introduce a theorem proving algorithm that uses practically no domain...
read it

First Experiments with Neural Translation of Informal to Formal Mathematics
We report on our first experiments to train deep neural networks that au...
read it

Machine Learning Guidance and Proof Certification for Connection Tableaux
Connection calculi allow for very compact implementations of goaldirect...
read it

Machine Learning Guidance and Proof Certification for Connection Tableau
Connection calculi allow for very compact implementations of goaldirect...
read it

Learning to Prove with Tactics
We implement a automated tactical prover TacticToe on top of the HOL4 in...
read it

Learning to Reason with HOL4 tactics
Techniques combining machine learning with translation to automated reas...
read it

HolStep: A Machine Learning Dataset for Higherorder Logic Theorem Proving
Large computerunderstandable proofs consist of millions of intermediate...
read it

Deep Network Guided Proof Search
Deep learning techniques lie at the heart of several significant AI adva...
read it

Semantic Parsing of Mathematics by Contextbased Learning from Aligned Corpora and Theorem Proving
We study methods for automated parsing of informal mathematical expressi...
read it

Monte Carlo Connection Prover
Monte Carlo Tree Search (MCTS) is a technique to guide search in a large...
read it

Proceedings First International Workshop on Hammers for Type Theories
This volume of EPTCS contains the proceedings of the First Workshop on H...
read it

Premise Selection and External Provers for HOL4
Learningassisted automated reasoning has recently gained popularity amo...
read it

Sharing HOL4 and HOL Light proof knowledge
New proof assistant developments often involve concepts similar to alrea...
read it

Certified Connection Tableaux Proofs for HOL Light and TPTP
In the recent years, the Metis prover based on ordered paramodulation an...
read it

Initial Experiments with TPTPstyle Automated Theorem Provers on ACL2 Problems
This paper reports our initial experiments with using external ATP on so...
read it

Developing Corpusbased Translation Methods between Informal and Formal Mathematics: Project Description
The goal of this project is to (i) accumulate annotated informal/formal ...
read it

Machine Learner for Automated Reasoning 0.4 and 0.5
Machine Learner for Automated Reasoning (MaLARea) is a learning and reas...
read it

Learningassisted Theorem Proving with Millions of Lemmas
Large formal mathematical libraries consist of millions of atomic infere...
read it

HOL(y)Hammer: Online ATP Service for HOL Light
HOL(y)Hammer is an online AI/ATP service for formal (computerunderstand...
read it

LearningAssisted Automated Reasoning with Flyspeck
The considerable mathematical knowledge encoded by the Flyspeck project ...
read it
Cezary Kaliszyk
is this you? claim profile
Researcher in the CL group at the University of Innsbruck