Theorem Proving System

"A mathematician is a device for turning coffee into theorems"--Erdős (see PaulErdos)

Disregarding the wit and wisdom of one of the 20th century's greatest mathematicians, a theorem proving system is a computer program (usually) designed to "prove theorems" from a set of facts and axioms (see AutomatedTheoremProving). Examples include PrologLanguage (see LogicProgramming), StructuredQueryLanguage, many TypeInference systems, etc.--they are far more commonplace that is often realized. And they remain an active area of research. (Currently, many programmers implement ad-hoc theorem proving systems--often without knowing what they're even doing theorem proving--to solve particular problems in a particular problem domain).

It should be noted that "theorem proving" does not (in general) refer to anything as grandiose as proving FermatsLastTheorem--instead it refers to being able to enter (usually simple) queries against a database of facts and axioms and being given an answer, derivable from the facts and axioms (as well as the basic laws of logic). In a type inference system (or any typechecker, really), a typical query might be "is A a subtype of B"?

Theorem proving is, in the general case, an undecidable problem (see GoedelsIncompletenessTheorem); though many specific problems are decidable. (One of the key questions in the study of TypeInference and typing systems in general is which type transforms make TypeInference undecidable and which don't. The reader is referred to TheoryOfObjects and other works in the literature on this subject for more details).