ATP is written and maintained by Adam Farquhar at the Stanford Knowledge Systems Lab . It is designed to be a reasonably efficient easy-to-use theorem prover for full first order logic and context logic. Axioms are expressed using the Knowledge Interchange Format (KIF).
ATP uses the model elimination theorem proving technique developed by Loveland. As discovered by Stickel, a model elimination thereom prover can be implemented by extending the implementation techniques employed by Prolog systems. The ATP implementation is based on the Prolog code described by Norvig in "Paradigms of AI Programming". The implementation also uses code for converting arbitrary first order logic sentences into clausal form from Russel and Norvig's "Artificial Intelligence: a Modern Approach".
ATP uses an iterative deepening search to find proofs. Iterative deepening performs a bounded depth first search for a solution on each iteration. If no solution is found at the current depth, then the the depth bound is increased and a depth first search is performed again. Because the search is bounded at each level, ATP cannot get lost on an endless path, such as Prolog might. Because the bound is gradually increased, ATP will eventually find a solution if there is one. The search is controlled by the variables *depth-start*, *depth-max*, and *depth-incr*.
ATP has a small number of variables that can be used to control the theorem proving: *ancestor-reduction*, *ancestor-cycle*, *occurs-check*, and *proof-collect*. Please see their documentation for more information about them. If all four of these variables are set to nil, then ATP is equivalent to a Prolog system.
Use the functions add-clause, add-clauses, add-fact, and add-facts to add clauses or facts to an ATP knowledge base. Facts are more heavily indexed than normal clauses and can be quickly retrieved. Currently, a predicate cannot be defined using both add-clause and add-fact . This limitation will be removed in later versions.
Use the macro ?- or the function finds to find a solution. The macro ?- provides interaction similar to the top level of a Prolog system. The function finds can be used for programmatic interactions.
Note that both the basic clauses and their contrapositives will be asserted by tell-kif.
Context logic theorem proving is achieved by translating the context logic sentence into first order logic. Use the kif-kb together with the functions tell-cl, finds-cl to assert and query in context logic. The function cl-to-kif performs the translation from context logic into KIF.
You may need to quote an infix expression. Typing #I( p(?x)) to the lisp reader will result in an error stating that P is an undefined function. Typing in '#I( p(?x) ) is likely to be what you meant.
The infixifier is a modified version of the one written by Kantrowitz and archived at ftp://ftp.cs.cmu.edu/user/ai/lang/lisp/code/syntax/infix.
Todo: add trace-expressions to the kb structure; change prolog to atp; have atp-kb remove duplicates on; assert; conditionalize adding ancestors correctly.
<- | Kb &Rest Clause | Function |
Add a <clause> of the form (head . body) to the <kb>. |
?- | Kb &Rest Goals | Function |
Prove <goals> in <kb> interacting with the user. |
Add-Clause | Clause-List Kb &Optional (Fact Nil) | Function |
Add a clause, <clause-list>, to <kb>. <clause-list> is a list (head . body) of atomic formulae. Normally, a clause is indexed under its head. If <fact> is T, then do a more complete indexing of the atom ground clause in the <kb>'s fact table. |
Add-Clauses | Kb Clauses | Function |
Add each clause in <clauses> to the <kb>. Each clause has the form (<- head . body). |
Add-Fact | Fact Kb | Function |
Add the atomic ground <fact> to the <kb>. |
Add-Facts | Facts Kb | Function |
Add each atomic ground fact in <facts> to the <kb>. |
Cl-Find | Pat Body &Rest Prove-Keywords &Key (Context (Quote Global)) &Allow-Other-Keys | Function |
For each proof of the context logic sentence <body>, return <pat>. Any keyword arguments for finds (which does the real work) may be used as well. |
Cl-Save | Cl-Sentence &Key (Context (Quote Global)) Kb (Contrapositives All) | Function |
Save the context logic sentence <cl-sentence> that holds in <context> into <kb>. Assert :all or :none of the <contrapostives>. |
Cl-To-Kif | S C | Function |
Translate the context logic sentence <s> that holds in context <c> into KIF. Prolog builtins including bagof and setof are handled correctly. |
Clear-Predicate | Predicate Kb | Function |
remove the clauses for a single predicate. |
Deref-Exp | Exp | Function |
Build something equivalent to <exp> with variables dereferenced. |
Drop-Fact | Fact Kb | Function |
Delete the atomic ground <fact> from the <kb>. |
Drop-Facts | Facts Kb | Function |
Delete each atomic ground fact in <facts> from the <kb>. |
Finds | Pat Body &Rest Prove-All-Keywords &Key Kb (Max All) &Allow-Other-Keys | Function |
Return a list of at most <max> bindings for <pat> satisfying <body> in <kb>. Return two values: list of results and T if there might be more solutions. Any of the keyword arguments to id-prove may also be provided to control the search. |
Finds-Cl | Pat Body &Rest Prove-Keywords &Key (Context (Quote Global)) &Allow-Other-Keys | Function |
For each proof of the context logic sentence <body>, return <pat>. Any keyword arguments for finds (which does the real work) may be used as well. |
Get-Clauses | X Kb &Optional (Facts-Too T) | Function |
Return all clauses in KB for the predicate mentioned in X. |
Id-Prove | Goals &Key Kb (Depth-Start *Depth-Start*) (Depth-Max *Depth-Max*) (Depth-Incr *Depth-Incr*) | Function |
Attempt to prove goals in the KB using iterative deepening. The iterative deepening search is controlled by depth-start, depth-max, and depth-incr, which have the same meanings as the global variables *depth-start*, *depth-max*, *depth-incr* respectively. |
Install-Builtins | Kb | Function |
Install links to builtin's and define basic predicates: member, append, or, and. |
Make-Kif-Kb | &Key (Title (Quote Nil)) (Clause-Queue (Make-Queue)) (Positive-Clauses (Make-Hash-Table)) (Negative-Clauses (Make-Hash-Table)) (Fact-Table (Make-Hash-Index Title Title)) (Sentence-Table (Make-String=-Trie)) (Sentence-Queue (Make-Queue)) (Form-Queue (Make-Queue)) (Axiom-Schemata (Quote Nil)) | Function |
Create a new atp kb capable that supports the assertion of arbitrary KIF sentences. Provide a <title> keyword for printing. |
Make-Prolog-Kb | &Key (Title (Quote Nil)) (Clause-Queue (Make-Queue)) (Positive-Clauses (Make-Hash-Table)) (Negative-Clauses (Make-Hash-Table)) (Fact-Table (Make-Hash-Index Title Title)) | Function |
Create a new atp kb. Provide a <title> keyword for printing. |
Prolog-Kb-All-Atoms | Kb | Function |
Return a list of all of the atoms in the kb that are not builtins only. |
Prove-All | Lists-Of-Goals Kb Depth Pos Neg Proof | Function |
Prove-all is the main routine of the prover. |
Tell-Cl | Cl-Sentence &Key (Context (Quote Global)) Kb (Contrapositives All) | Function |
Save the context logic sentence <cl-sentence> that holds in <context> into <kb>. Assert :all or :none of the <contrapostives>. |
Tell-Kif | Kb Kif-Form &Key (Contrapositives All) | Function |
Assert a <kif-form> into a KIF <kb>. This function first converts the <kif-form> into a closed sentence. It then converts this sentence into clausal form and asserts each of the clauses into the <kb>. If <contrapositives> is :all, the contrapositives of the clauses are added as well. In addition, every asserted clause has a link to the sentence that it came from. This helps when, for instance, a proof is displayed. |
Top-Level-Prove | Goals Kb | Function |
A top level function to prove the atomic <goals> are true in the <kb>. |
*Ancestor-Cycle* | Variable | |
When nil, do not peform a circularity check to determine if the current goal is the same as one already on the stack. This check may substantially reduce the search space for some problems, but is expensive for problems that involve deep recursion. The value of *ancestor-cycle* will not effect the correctness or completeness of the theorem proving. |
*Ancestor-Reduction* | Variable | |
When nil, do not perform the model elimination ancestor reduction. If the ancestor check is not performed, then inference may not be complete. Problems involving disjunction will not be solved. |
*Ancestors* | Variable | |
When nil, do not perform the model elimination ancestor check. If the ancestor check is not performed, then inference may not be complete. Problems involving disjunction will not be solved. |
*Circularity* | Variable | |
When nil, do not peform a circularity check to determine if the current goal is the same as one already on the stack. This check may substantially reduce the search space for some problems, but is expensive for problems that involve deep recursion. The value of *circularity* will not effect the correctness or completeness of the theorem proving. |
*Depth-Incr* | Variable | |
The depth increment for the iterative deepening search. If there are no more solutions at the current depth, the depth bound is increased by *depth-incr*. |
*Depth-Max* | Variable | |
The maximum depth for the iterative deepening search. No solution of cost greater than *depth-max* will ever be considered. |
*Depth-Start* | Variable | |
The initial depth limit for the iterative deepening search. Initially solutions of cost up to *depth-start* will be considered. |
*Inference-Count* | Variable | |
The number of unifications performed and builtins executed since last reset by top-level-prove or finds. |
*Occurs-Check* | Variable | |
When nil, do not perform an occurs check during unification. Working without an occurs check is faster, but can be unsound. |
*Proof-Collect* | Variable | |
When nil, do not collect a proof tree during execution. The proof tree can be printed out when the user has called ATP with ?-. |
*Search-Cut-Off* | Variable | |
The value of *search-cut-off* will be set to T if the search was cut during at the current iteration due to a depth limit. If *search-cut-off* is T, then there may be more solutions of greater cost. If it is NIL, however, there are no more solutions. |
Kif-Kb | Structure | |
The structure that defines a kif-kb. It supports the assertion of arbitrary KIF sentences. |
Prolog-Kb | Structure | |
The structure that defines the atp kb. |
= | Logic | |
(= ?x ?y). Unify ?x and ?y. |
Apply | Logic | |
(apply <function> <expr>). Apply lisp <function> to <expr>, which may contain variables. |
Atom | Logic | |
(atom <x>). Succeed if <x> is a lisp atom (not a list). |
Bagof | Logic | |
(bagof <pat> <clauses> <list>). Try to solve <clauses>. For each solution, collect <pat> into <list>. |
Bagofn | Logic | |
(bagofn <max> <pat> <clauses> <list>). Try to solve <clauses>. For up to <max> solutions, collect <pat> into <list>. |
Call | Logic | |
(call <goal>). Try to solve <goal>. |
Cut | Logic | |
(cut). The Prolog cut. Any attempt to backtrack over a cut will result in the parent clause failing. See any Prolog book for a discussion of cut and its semantics. |
Is | Logic | |
(is <var> <expression>). Bind <var> with the result of evaluating lisp <expression>. |
Nonvar | Logic | |
(nonvar <x>). Succeed if <x> is not an unbound logic variable. |
Numberp | Logic | |
(numberp <x>). Succeed if <x> is a number. |
Read | Logic | |
(read <exp>). Bind <exp> with the results of reading from the *standard-input* stream. |
Repeat | Logic | |
(repeat). Always succeed. Used to construct loops. |
Setof | Logic | |
Like bagof, except results are unique. |
Test | Logic | |
(test <function> . <args>). Fails if applying <function> to <args> returns nil. |
Unp | Logic | |
(unp <goals>). The list of goals cannot be proven under current bounds. |
Var | Logic | |
(var <x>). Succeed if <x> is an unbound logic variable. |
Write | Logic | |
(write <exp>). Write <exp> on to *standard-out* using write. |