TheoScrutor.

Even though only a tiny fraction of formalized mathematical knowledge is available our current retrieval methods are already inadequate for knowledge reuse: Inside a single library, it is often simpler to reprove a theorem than finding an equivalent or stronger one to reference.

TheoScrutor is a search engine for theory inclusions for the purpose of theorem reuse. A target theory T is said to include a source theory S via a signature translation t iff the t-translated axioms from S are theorems in T. If T includes S via t then all the t-translated theorems from S hold in T without out any extra proof of those theorems - i.e. theorems from S can be reused in T.

TheoScrutor tries to find for a given source theory S pairs (t,T) such that T includes S via t and thus enables theorem reuse from S in T. Since the proof of theory inclusions is undecidable in general, TheoScrutor's search is based on a weaker notion of theory inclusions: All pairs (t,T) for a source theory S such that the t-translated axioms of S exist in T modulo an equational theory.

TheoScrutor's search technique is based on formula normalization, standardization, and separation of structure and parameter in formulae. Formulae structures serve as efficient prefilter via hash tables. TheoScrutor finds for instance in a formalized library of 1.5 million formulae about 300 theory inclusions within 0.2 seconds.

As soon as TheoScrutor's graphical user interface is mature and tested with lots of theory inclusion searches it will go on-line.