Automated Theory Interpretation

  • This thesis presents novel methods from automated reasoning to find reusable knowledge and knowledge overlaps in large formalized knowledge bases. The focus is on formalized mathematics, but the methods are applicable on any kind of formalized content as long as the application of classical logic inference rules on this content is admissible. Formalized as well as traditional mathematics is advantageously organized in theories as its biggest knowledge units. As history of mathematics has shown, appearently unrelated theories happen to share a common core (i.e. knowledge overlap) once the concepts of each theories are translated appropriately. If all valid sentences of a theory A also hold in another theory B with an appropriate translation T, then A is said to be included in B -- or A can be interpreted in B. Since all sentences of a theory are derivable from a few of it, namely from its axioms, we know that A is included in B as soon as we have shown that the axioms of A hold in B. In this case all derivable sentences in A automatically hold in B too, i.e.the knowledge from A can be reused in B. In this thesis an algorithm for automated theory interpretation search is presented. It is based on semantic formula matching by means of normalization taken from term rewriting and a novel standardization technique for associative and commutative terms. Moreover, a practical notion of theory intersection is introduced and an algorithm for the construction of such intersections is presented. Both algorithms are implemented in a prototype system and experiments are conducted on the largest library of formalized mathematics -- the Mizar Mathematical Library -- which demonstrates the scalability of the algorithms and also reveal thousands of theory interpretations.

Download full text

Cite this publication

  • Export Bibtex
  • Export RIS

Citable URL (?):

Search for this publication

Search Google Scholar Search Catalog of German National Library Search OCLC WorldCat Search Catalog of GBV Common Library Network Search Catalog of Jacobs University Library Search Bielefeld Academic Search Engine
Meta data
Publishing Institution:IRC-Library, Information Resource Center der Jacobs University Bremen
Granting Institution:Jacobs Univ.
Author:Immanuel Normann
Referee:Michael Kohlhase, Herbert Jaeger, Till Mossakowski
Advisor:Michael Kohlhase
Persistent Identifier (URN):urn:nbn:de:101:1-201305237003
Document Type:PhD Thesis
Date of Successful Oral Defense:2008/12/08
Year of Completion:2008
Date of First Publication:2009/12/08
PhD Degree:Computer Science
School:SES School of Engineering and Science
Library of Congress Classification:Q Science / Q Science (General) / Q300-390 Cybernetics / Q325-342 Self-organizing systems. Conscious automata / Q334-342 Artificial intelligence
Call No:Thesis 2008/35

$Rev: 13581 $