![[Home]](/ailab/people/andel/pics/AIWiki.png)
A theorem-proving program starts with a set of propositions, which are the initial set of known facts. And it usually has a goal proposition, that is, a proposition which it needs to prove. It must logically derive the goal proposition from the other propostions.
The program applies a logical rule to the initial propositions, to logically derive a conclusion, i.e. a new proposition. The program applies rules repeatedly, to draw one conclusion after another.
Example: I know that “all men are mortal”. I know that “Socrates is a man”. So I’ll add “Socrates is mortal” to my knowledgebase.
It does this until it manages to conclude the goal proposition, the one that it needs to prove.
(Or, sometimes, it applies rules until it discovers that the goal proposition cannot be proved. Or it applies rules until it runs out of time.)
It has a set of rules available to it, and it has to choose which rules to apply, in which order, to conclude the goal proposition. It has to be able to cope with paths which lead to dead-ends, and it has to be able to avoid infinite loops, which would prevent it reaching its goal.
TheoremProving is the most obvious method of reasoning with a LogicalRepresentation.
Proving theorems is related to Planning. Theorem proving programs and planning programs use similar code. Both types of program can make plans, i.e. they find a series of steps that lead to a goal.
A theorem proving program uses steps called “rules” to step from known facts to derived facts. Whereas a planning program uses steps called “actions” that will change a set of facts in the real world. – MartinSondergaard.
A related/broader area is AutomatedTheoryFormation, that is, trying to discover (interesting/useful) new theorems and conjectures.
There is a popular theorem prover called Otter.
Otter is written in Prolog. If I recall correctly, source code is available. It uses Prolog facts that look like propositions in the Predicate Calculus. Otter can prove propositions that are expressed in the Predicate Calculus. (For info on the Predicate Calculus see PredicateLogic.) I haven’t used Otter myself, because I no longer want to use the Predicate Calculus. – MartinSondergaard.
Apparently there is a technique called “partitioning” for detecting and exploiting the implicit structure in logical knowledgebases – I think it means you partition a large knowledgebase into a bunch of smaller subknowedgebases and do inference as you can within those subknowedgebases, crossing between them as rarely as possible. See
http://www.ksl.stanford.edu/projects/RKF/Partitioning/