Automated Theory Interpretation
Immanuel Normann · 2009
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.