Cezary Kaliszyk

research

∙ 03/12/2023

MizAR 60 for Mizar 50

As a present to Mizar on its 50th anniversary, we develop an AI/TP syste...

0 Jan Jakubův, et al. ∙

research

∙ 08/13/2022

Differentiable Inductive Logic Programming in High-Dimensional Space

Synthesizing large logic programs through Inductive Logic Programming (I...

0 Stanisław J. Purgał, et al. ∙

research

∙ 05/13/2022

Lash 1.0 (System Description)

Lash is a higher-order automated theorem prover created as a fork of the...

0 Chad E. Brown, et al. ∙

research

∙ 05/04/2022

The Isabelle ENIGMA

We significantly improve the performance of the E automated theorem prov...

0 Zarathustra A. Goertzel, et al. ∙

research

∙ 04/26/2022

Formalizing a Diophantine Representation of the Set of Prime Numbers

The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step i...

0 Karol Pąk, et al. ∙

research

∙ 04/06/2022

Adversarial Learning to Reason in an Arbitrary Logic

Existing approaches to learning to prove theorems focus on particular lo...

0 Stanisław J. Purgał, et al. ∙

research

∙ 12/29/2021

Learning Higher-Order Programs without Meta-Interpretive Learning

Learning complex programs through inductive logic programming (ILP) rema...

0 Stanisław J. Purgał, et al. ∙

research

∙ 07/21/2021

JEFL: Joint Embedding of Formal Proof Libraries

The heterogeneous nature of the logical foundations used in different in...

0 Qingxiang Wang, et al. ∙

research

∙ 04/12/2021

Online Machine Learning Techniques for Coq: A Comparison

We present a comparison of several online machine learning techniques fo...

0 Liao Zhang, et al. ∙

research

∙ 01/25/2021

Disambiguating Symbolic Expressions in Informal Documents

We propose the task of disambiguating symbolic expressions in informal S...

0 Dennis Müller, et al. ∙

research

∙ 01/22/2021

A Study of Continuous Vector Representationsfor Theorem Proving

Applying machine learning to mathematical terms and formulas requires a ...

0 Stanisław Purgał, et al. ∙

research

∙ 05/26/2020

A Survey of Languages for Formalizing Mathematics

In order to work with mathematical content in computer systems, it is ne...

0 Cezary Kaliszyk, et al. ∙

research

∙ 12/05/2019

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

In this paper we share several experiments trying to automatically trans...

0 Qingxiang Wang, et al. ∙

research

∙ 11/27/2019

Property Invariant Embedding for Automated Reasoning

Automated reasoning and theorem proving have recently become major chall...

0 Miroslav Olšák, et al. ∙

research

∙ 11/07/2019

Can Neural Networks Learn Symbolic Rewriting?

This work investigates if the current neural architectures are adequate ...

0 Bartosz Piotrowski, et al. ∙

research

∙ 05/30/2019

Towards Finding Longer Proofs

We present a reinforcement learning (RL) based guidance system for autom...

0 Zsolt Zombori, et al. ∙

research

∙ 03/06/2019

GRUNGE: A Grand Unified ATP Challenge

This paper describes a large set of related theorem proving problems obt...

0 Chad E. Brown, et al. ∙

research

∙ 08/20/2018

Concrete Semantics with Coq and CoqHammer

The "Concrete Semantics" book gives an introduction to imperative progra...

0 Łukasz Czajka, et al. ∙

research

∙ 05/19/2018

Reinforcement Learning of Theorem Proving

We introduce a theorem proving algorithm that uses practically no domain...

0 Cezary Kaliszyk, et al. ∙

research

∙ 05/10/2018

First Experiments with Neural Translation of Informal to Formal Mathematics

We report on our first experiments to train deep neural networks that au...

0 Qingxiang Wang, et al. ∙

research

∙ 05/08/2018

Machine Learning Guidance and Proof Certification for Connection Tableaux

Connection calculi allow for very compact implementations of goal-direct...

0 Michael Färber, et al. ∙

research

∙ 05/08/2018

Machine Learning Guidance and Proof Certification for Connection Tableau

Connection calculi allow for very compact implementations of goal-direct...

0 Michael Färber, et al. ∙

research

∙ 04/02/2018

Learning to Prove with Tactics

We implement a automated tactical prover TacticToe on top of the HOL4 in...

0 Thibault Gauthier, et al. ∙

research

∙ 04/02/2018

Learning to Reason with HOL4 tactics

Techniques combining machine learning with translation to automated reas...

0 Thibault Gauthier, et al. ∙

research

∙ 03/01/2017

HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

Large computer-understandable proofs consist of millions of intermediate...

0 Cezary Kaliszyk, et al. ∙

research

∙ 01/24/2017

Deep Network Guided Proof Search

Deep learning techniques lie at the heart of several significant AI adva...

0 Sarah Loos, et al. ∙

research

∙ 11/29/2016

Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving

We study methods for automated parsing of informal mathematical expressi...

0 Cezary Kaliszyk, et al. ∙

research

∙ 11/18/2016

Monte Carlo Connection Prover

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

0 Michael Färber, et al. ∙

research

∙ 06/17/2016

Proceedings First International Workshop on Hammers for Type Theories

This volume of EPTCS contains the proceedings of the First Workshop on H...

0 Jasmin Christian Blanchette, et al. ∙

research

∙ 09/11/2015

Premise Selection and External Provers for HOL4

Learning-assisted automated reasoning has recently gained popularity amo...

0 Thibault Gauthier, et al. ∙

research

∙ 09/11/2015

Sharing HOL4 and HOL Light proof knowledge

New proof assistant developments often involve concepts similar to alrea...

0 Thibault Gauthier, et al. ∙

research

∙ 10/20/2014

Certified Connection Tableaux Proofs for HOL Light and TPTP

In the recent years, the Metis prover based on ordered paramodulation an...

0 Cezary Kaliszyk, et al. ∙

research

∙ 06/06/2014

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

This paper reports our initial experiments with using external ATP on so...

0 Sebastiaan Joosten, et al. ∙

research

∙ 05/14/2014

Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description

The goal of this project is to (i) accumulate annotated informal/formal ...

0 Cezary Kaliszyk, et al. ∙

research

∙ 02/11/2014

Machine Learner for Automated Reasoning 0.4 and 0.5

Machine Learner for Automated Reasoning (MaLARea) is a learning and reas...

0 Cezary Kaliszyk, et al. ∙

research

∙ 02/11/2014

Learning-assisted Theorem Proving with Millions of Lemmas

Large formal mathematical libraries consist of millions of atomic infere...

0 Cezary Kaliszyk, et al. ∙

research

∙ 09/19/2013

HOL(y)Hammer: Online ATP Service for HOL Light

HOL(y)Hammer is an online AI/ATP service for formal (computer-understand...

0 Cezary Kaliszyk, et al. ∙

research

∙ 11/29/2012

Learning-Assisted Automated Reasoning with Flyspeck

The considerable mathematical knowledge encoded by the Flyspeck project ...

0 Cezary Kaliszyk, et al. ∙

Cezary Kaliszyk

Featured Co-authors