AUTOKNOMATH · Automated reasoning in large formal mathematical knowledge bases

Final Activity Report Summary - AUTOKNOMATH (Automated Reasoning in Large Formal Mathematical Knowledge Bases)

The AUTOKNOMATH project provided a significant connection between two important fields of computer-supported reasoning, namely computer-assisted formalisation of mathematics and automated reasoning. This connection in turn allowed for significant development of novel AI methods, like machine learning in the field of automated reasoning. The largest available formal mathematical knowledge base, i.e. the Mizar mathematical library, was translated to the TPTP format which was used by state-of-the-art first-order automated theorem provers (ATPs). The Mizar problems for theorem proving (MPTP) system was developed, providing a number of functionalities for translating Mizar to first-order logic, generating ATP problems consistently, analysing results, etc. This effort was complemented by developing strong methods for reasoning in large theories and designing and organizing competitions in this field. The MPTP $ 100 Challenge was, in 2007, the first automated reasoning competition allowing the participants to work in a large-theory context and to use under clear conditions complementary AI approaches like machine learning from previous solutions. This was followed in 2008 by the establishment of the large theory batch division of the world championship in automated theorem proving (CASC), where the conditions were similar to the MPTP Challenges. The Mizar (MPTP) problems were already joined in this competition by problems from large formal ontologies, such as SUMO and Cyc. The success rate of re-proving the Mizar theorems by ATP systems was raised, during the course of the project, from 39 % to 61 %. The success rate for re-proving the Mizar atomic steps by ATPs reached 99.8 % and made ATP-based cross-verification of large parts of the Mizar library feasible. The entire set of 252 Mizar problems used for the MPTP challenge was ATP-verified in this way. Moreover, the development of the 'MaLARea' system initiated, combining machine learning, automated theorem proving and model finding in a novel kind of inductive and deductive AI loop. This system was not only novel, but also very strong for proving problems in large theories. It was the strongest system for the MPTP challenge and won the MZR category of the 2008 CASC competition, solving 1.5 times more problems than the second best system. The transfer of knowledge was realised in several ways during this project. The joint work of researcher with the outgoing host group was crucial for achieving the abovementioned results and several jointly authored papers were published. The work on reasoning in large mathematical theories coincided with independent work on reasoning over large formal ontologies like SUMO and Cyc, leading to a new joint division of the main automated reasoning competition. The transfer of these research topics to the return host caused the development of the 'SInE' system by Dr Urban student Krystof Hoder. This system is now the strongest system for reasoning over the SUMO formal ontology.

Data: CORDIS, © European Union