10 papers
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…
Fast and Slow Enigmas and Parental Guidance
Zarathustra Goertzel, Karel Chvalovský, Jan Jakubův +2
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding se…
Learning to solve geometric construction problems from images
J. Macke, J. Sedlar, M. Olsak +2
We describe a purely image-based method for finding geometric constructions with a ruler and compass in the Euclidea geometric game. The method is based on adapting the Mask R-CNN…
The Role of Entropy in Guiding a Connection Prover
Zsolt Zombori, Josef Urban, Miroslav Olšák
In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where…
ω-categorical structures avoiding height 1 identities
Manuel Bodirsky, Antoine Mottet, Miroslav Olšák +3
The algebraic dichotomy conjecture for Constraint Satisfaction Problems (CSPs) of reducts of (infinite) finitely bounded homogeneous structures states that such CSPs are polynomial…
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
Miroslav Olšák
Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the hum…