Worldchampionship in Automated Reasoning: computer scientist awarded
Publié le mercredi 04 septembre 2019
On the occasion of the annual World Championship for Automatic Theorem Proving (“CADE ATP System Competition”, in short CASC) which took place on 2829 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for “LeoIII”, a computer software that proves mathematical conjectures autonomously. Automatic reasoningLeoIII has been developed since 2014 by Alexander Steen, postdoc researcher within the Computer Science and Communications Research Unit (CSC) at the University of Luxembourg. “LeoIII is a computer software that we call "automated theorem prover" or, more general, a reasoning system that tries to find proofs for mathematical conjectures completely autonomously, that is without any help or advice from humans. The input of such systems is a problem statement in a formal logical language, and the output is  if successful – a formal proof of that conjecture”, explains Alexander. Applications in mathematics and beyondTheorem provers are used by mathematicians and computer scientists to formalise and to find proofs. In the first case, the human can input a proof of a mathematical statement and the system will check it for correctness; in the latter case, the proof is generated by the system in full. Specifically, LeoIII automated a logical language which is referred to as "higherorder logic", which is a very expressive formalism that can capture even more applications; but is also harder to realise in practice. Recently, Christoph Benzmüller, Professor at Freie Universität Berlin, Germany, and affiliated with the University of Luxembourg, has applied such systems to assess e.g. philosophical arguments from metaphysics. “I am currently working on applying this technology to reasoning in the context of computer ethics and normative applications. With this step, of course, the target audience will eventually be even wider than just mathematicians and computer scientists”, adds Alexander. International recognitionLeoIII ranked first place in the category "Large Theory Batch" (LTB) during the annual World Championship for Automatic Theorem Proving with over 54% solved problems (5441 out of 10000). “I am very happy about the good performance that LeoIII demonstrated in the LTB category, that has classically been dominated by firstorder provers in the last years. This is a strong indication that the extra efforts of automating higherorder logic come with convincing benefits in practical applications”. The next best systems, the world leading firstorder provers E (DHBW Stuttgart) and Vampire (U Manchester) found roughly 15% and 17% less solutions, respectively. LeoIII also ranked second place in the smaller THF division. LeoIII is opensource software and freely available for use and further development. Details on the system and its theoretical foundations can be found in Steen’s PhD thesis. More information: http://page.mi.fuberlin.de/lex/leo3/ 


URL: https://wwwfr.uni.lu/universite/actualites/a_la_une/world_championship_in_automated_reasoning_computer_scientist_awarded  Date: mercredi 19 février 2020 19:49:54 