4 papers · 1 filter
Reintroducing the Second Player in EPR
Leroy Chew, Mikoláš Janota, Miroslav Olšák +1
In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (E…
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…
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…
Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems)
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…