Computer Scientists from Freie Universität Are Vice World Champions in Automated Theorem Proving
Automated Theorem Prover (ATP) Leo-III Developed at Freie Universität Berlin Took Second Place in Higher-Order Logic Category in World Championship
№ 223/2017 from Aug 21, 2017
The Leo-III computer system has been under development since 2014 by researchers Alexander Steen and Max Wisniewski under the direction of Dr. Christoph Benzmüller at the Dahlem Center for Machine Learning and Robotics at the Institute of Computer Science, Freie Universität Berlin. At the beginning of August, the system was tested at the CADE ATP System Competition 2017 in Gothenburg, Sweden, and correctly solved 382 of the 500 tasks, thus finishing in second place.
Automated theorem provers are computer programs that receive a set of assumptions - called axioms - and are given a predetermined time to try automatically to find a formal mathematical proof of the validity of a particular conjecture. For this purpose the assumptions as well as the conjecture are formulated in a specific mathematical logic formalism. In the annual world championship of theorem provers, the CADE ATP System Competition, the best of such computer programs compete against each other in different categories and try to solve as many as possible of 500 randomly selected problems. Leo-III competes in a particularly challenging category of theorem proving, in which many aspects are the subject of current basic research. Nevertheless, the comparatively young Leo-III managed to prove 382 of the 500 tasks as correct. The only ATP that was able to solve more tasks was Satallax, a system developed at the University of Innsbruck and Czech Technical University of Prague. The development of Leo-III was funded by the German Research Foundation (DFG). Leo-III is freely accessible as open source software.
Contact
Alexander Steen, Dahlem Center for Machine Learning and Robotics, Institute of Computer Science, Freie Universität Berlin, Tel.: +49 30 838-75101, Email: a.steen@fu-berlin.de