22 citations · 55 across the 10 of their papers we have counts for
Showing 2020Show all
3 papers · 1 filter
math.LO2020★ 9 cited
ω-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…
cs.LO2020
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…
cs.AI2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…