4 papers
Machine Learning Meets The Herbrand Universe
Jelle Piepenbrock, Josef Urban, Konstantin Korovin +3
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT sol…
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…
Local loop lemma
Miroslav Olšák
We prove that an idempotent operation generates a loop from a strongly connected digraph containing directed cycles of all lengths under very mild (local) algebraic assumptions. Us…
Loop conditions with strongly connected graphs
Miroslav Olšák
We prove that the existence of a term satisfying in a general algebraic structure is equivalent to an existence of a term satisfying $t(x,x,y,y,z,…