ICIS Foundations Group  [Foundations FrontPage] [TitleIndex] [WordIndex]

Research/Learning2Reason

Learning2Reason

What?

Who?

The project is carried out at the Intelligent Systems section at RU Nijmegen. Both the Machine Learning group and the Foundations group participate in the project, each bringing their expertise. The current contributors are:

Background to the Research

In recent years, large corpora of formally expressed knowledge have become available in the fields of formal mathematics, software verification, and real-world ontologies. Examples of such formal mathematical libraries are the Mizar Mathematical Library, the Constructive Coq Repository at Nijmegen, the Flyspeck project, the The Archive of Formal Proofs, and the Mathematical Components project. Real-world ontologies include for example the Cyc Knowledge Base, the Suggested Upper Merged Ontology (SUMO), and the YAGO semantic knowledge base. To derive new knowledge from such large corpora, one uses computer-assisted and automated reasoning methods, which typically use one-problem-at-a-time approaches (e.g., resolution and tableaux proving). This symbolic (or deductive) approach typically does not consider the knowledge contained in previous proofs, and it suffers from a fast-growing search space.

This makes computer-assisted reasoning a suitable domain for complementary heuristic (or inductive) AI approaches, like machine learning, which rely on learning from the large amount of previous knowledge to heuristically control the search space, e.g., by estimating the usefulness of existing lemmas for proving a new result.

The Basis

A starting point for the project are several datasets extracted from the Mizar Mathematical Library, and existing state-of-the-art machine learning and automated reasoning methods. We evaluate these methods on the datasets, adapt them to the specifics of the mathematical domains, and combine them together in novel metasystems like the Machine Learner for Automated Reasoning. We are also interested in getting mathematical datasets coming from other systems, and in experimenting with different learning and reasoning tools.

The Tasks

Our focus so far has been on the following tasks:

The Results

Our current prototypes/systems/evaluations and software developed so far are:

Publications


2013-06-07 12:15