Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
Josef Urban, Robert Veroff · EPiC series in computing · 2018
We describe our experiments with several state-of-the-art automated theorem provers on the problems in Tarskian Geometry created by Beeson and Wos. In comparison to the manually-guided Otter proofs by Beeson and Wos, we can solve a large number of problems fully automatically, in particular thanks to the recent large-theory reasoning methods.