This is an attempt at a brief initial overview of the state of the art in the young eld of rst-order automated reasoning in large theories (ARLT). It is necessarily biased by the author's imperfect knowledge, and hopefully will serve as material provoking further corrections and completions. Why should we want to (automatically) reason in large theories and develop them instead of small theories? Here are several answers: Mathematicians work in large theories. They know a lot of concepts, facts, examples and counter-examples, proofs, heuristics, and theory-development methods. Other scientists (and humans in general) work with large theories. Consider physics, chemistry, biology, law, politics, large software libraries, Wikipedia, etc. Our current knowledge about the world is large. In the last years, more and more knowledge is becoming available formally by all kinds of human e orts (interactive theorem proving, common-sense reasoning, knowledge bases for various sciences, Semantic Web, etc.). This is an opportunity for automated reasoning to help with the sciences and tasks mentioned above. Existing resolution/superposition automated reasoning systems often derive large numbers of facts, even from small initial number of premises. Managing such large numbers can pro t from specialized large-theory techniques.
1.1 and likely (in less explicit form), also a large amount of general problem-solving knowledge that the automated reasoning eld should reveal and integrate into its pool of methods.
For this, however, another limited view needs to be overcome: Large theories (and theories in general) are not just random collections of usable facts. Mathematical theories in particular have been developed by smart people over centuries, and quite likely such theories are the best, deeply computer-understandable corpus of abstract human thinking that we currently have. It seems negligent to ignore the internal theory structure, and the problem-solving and theoryengineering knowledge developed by mathematicians so far. Especially when we know that rst-order ATP is an undecidable problem, and that the current ATP methods are on average far behind what trained mathematicians can do.
Thus, large complex formal theories and knowledge bases are not an enemy, but an opportunity. Not just an opportunity to reason with the knowledge of many already established facts, but also an opportunity to analyze and learn how smart people reason and prove di cult theorems, develop their conceptual space, and how they nd surprising connections and solutions. In short, large formal theories are a great new playground for developing general AI. But because general AI (and theorem-proving oriented AI in particular) has been in the second half of the 20th century labeled as unproductive, general AI research in this eld should go hand-in-hand with practical applications and usability testing. So far, this has fortunately often been the case in this young eld. 2
Several large formal knowledge bases have become recently available to experiments with rstorder automated reasoning tools. To name the major ones (in alphabetic order):
It is likely that more will follow (or already are available). For example, the HOL
Light/Flyspeck [
The corpora di er in their purpose/origin, size, complexity, consistency, completeness, and the extent to which they cover various large-theory aspects. The common-sense ontologies contain a lot of classi cation/hierarchical knowledge, resulting typically in simple Horn clauses, and also a lot of concept de nitions with relatively few facts proved about them. Storing and maintaining proofs has so far been a secondary aspect. Their primary emphasis was not (so far) on building up libraries of more and more advanced proved theorems about the world, but rather on covering as many concepts as possible by suitable de nitions.
On the other hand, the mathematical theories have a much larger number of nontrivial mathematical theorems in them, and their formal content typically follows some established informal theory developments based on well-known and xed mathematical foundations. There is more concept/fact re-use in mathematics, and nontrivial proofs of many facts exist and (at least in theory) can be made available in common formats and for large-theory techniques based on inspection of previous proofs and theory developments. 3
The existing large-theory reasoning methods can be divided into several groups, using various criteria. One criterion is the method used for knowledge selection. The methods developed so far include syntactic heuristics, heuristics using semantic information, methods that look at previous solutions, and combinations thereof. Systems and methods that make use mainly of syntactic criteria for premise selection include:
The SInE (SUMO Inference Engine) algorithm by Krystof Hoder [
The Conjecture Symbol Weight clause selection heuristics in E prover [
A method which is purely signature-based, however the word semantics appears in it, is latent semantics. Latent semantics is a machine learning method that has been successfully used for example in the Net ix Challenge, and in web search. Its principle is to automatically derive \semantic" equivalence classes of words (like car, vehicle, automobile ) from their co-occurrences in documents, and to use such equivalence classes (also called synsets in the WordNet ontology) instead of the original words for searching and related tasks. This technique has been so far used in:
Yuri Puzis' initial relevance ordering of premises used in the SRASS ATP metasystem [
MaLARea is also an example of a system that uses learning from previous proofs for guiding
premise-selection for new conjectures. The idea of this approach is to de ne suitable features
characterizing conjectures (symbolic, semantic, structural, etc.), and to use machine learning
methods on available proofs to learn the function that associates the conjecture features with
the relevant premises. A sophisticated learning approach has been suggested and implemented in
E prover by Stephan Schulz for his PhD work [
Note that such techniques already move the large-theory techniques towards smart
generalpurpose ATP techniques for proof guidance. A recent attempt in this direction is the MaLeCoP
system [
Not all systems do premise selection, however they may be still worth of mentioning.
One way how to reason with full large theories is to signi cantly limit the reasoning power.
At the extreme, such methods become the many search methods available for the corpora
mentioned above. A somewhat more involved memorization/reasoning technique is subsumption
implemented in various ATP systems. A type-aware extension of subsumption is implemented
for the Mizar library in the MoMM system [
3The author and Stephan Schulz have shortly tried to revive this old E code and test it on the MPTP Challenge benchmark in 2007, however without any signi cant results. So this advanced code is still waiting to be properly revived and tested.
Another interesting large-theory techniques is lemmatization and concept creation. An
example lemmatization system has been implemented by Petr Pudlak in his PhD thesis [