29 citations · 56 across the 17 of their papers we have counts for
4 papers · 1 filter
Lash 1.0 (System Description)
Chad E. Brown, Cezary Kaliszyk
Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules…
The Isabelle ENIGMA
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk +3
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In parti…
Formalizing a Diophantine Representation of the Set of Prime Numbers
Karol Pąk, Cezary Kaliszyk
The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert's 10th problem. Almost three decades of work on the problem have result…
Adversarial Learning to Reason in an Arbitrary Logic
Stanisław J. Purgał, Cezary Kaliszyk
Existing approaches to learning to prove theorems focus on particular logics and datasets. In this work, we propose Monte-Carlo simulations guided by reinforcement learning that ca…