# Atp System Reference Manual

## Introduction

Adam's Automated Theorem Prover (ATP) provides a facility for proving theorems in first order logic from a set of axioms.

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.

### Using ATP with Full First Order Logic

The theorem proving technique use by ATP is complete for first order logic. The basic prolog-kb, however, only accepts clauses as input. Use the kif-kb structure and the function tell-kif to assert arbitrary KIF sentences. The original KIF sentence and the clausal form are stored in the kif-kb.

Note that both the basic clauses and their contrapositives will be asserted by tell-kif.

### Using ATP with Context Logic

ATP also supports context logic as developed by Buvac and McCarthy. Context logic extends first order logic with a modality ist (read 'is true') that takes a context and a sentence as arguments. Informally it means that the sentence is true in the given context.

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.

### Infix Syntax

In addition to the standard KIF syntax, ATP includes a reader for an infix notation. #I( forall(?x, p(?x)) ) is translated into the KIF (forall ?x (p ?x)). Any characters surrounded by #I( ... ) will be
parsed by the infix reader. The logic syntax includes: not, ~, and, &, ^, or, |, < =>, =>, < =; as well as the arithmetic operators +, -, *, %. The set notation {a,b,...} translates to (setof a b...) and [a,b,...] becomes (listof a b ...).

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.

### KSL Site Information

ATP is now built into the basic KSL lisp band, cms. The most recent version of the band can be found at "/a/htw/bands/cms". The system is defined in the ATP package. When working with the system, you may want to work within the ATP package, or ensure that your package uses the ATP package.

The functions ->cnf, ->pttp, and their friends may be useful for manipulating logical sentences.

Todo: add trace-expressions to the kb structure; change prolog to atp; have atp-kb remove duplicates on; assert; conditionalize adding ancestors correctly.

## Functions And Macros

 <- Kb &Rest Clause Function Add a of the form (head . body) to the .

 ?- Kb &Rest Goals Function Prove in interacting with the user.

 Add-Clause Clause-List Kb &Optional (Fact Nil) Function Add a clause, , to . is a list (head . body) of atomic formulae. Normally, a clause is indexed under its head. If is T, then do a more complete indexing of the atom ground clause in the 's fact table.

 Add-Clauses Kb Clauses Function Add each clause in to the . Each clause has the form (<- head . body).

 Add-Facts Facts Kb Function Add each atomic ground fact in to the .

 Cl-Find Pat Body &Rest Prove-Keywords &Key (Context (Quote Global)) &Allow-Other-Keys Function For each proof of the context logic sentence , return . 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 that holds in into . Assert :all or :none of the .

 Cl-To-Kif S C Function Translate the context logic sentence that holds in context 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 with variables dereferenced.

 Drop-Fact Fact Kb Function Delete the atomic ground from the .

 Drop-Facts Facts Kb Function Delete each atomic ground fact in from the .

 Finds Pat Body &Rest Prove-All-Keywords &Key Kb (Max All) &Allow-Other-Keys Function Return a list of at most bindings for satisfying in . 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 , return . 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 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 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 that holds in into . Assert :all or :none of the .

 Tell-Kif Kb Kif-Form &Key (Contrapositives All) Function Assert a into a KIF . This function first converts the into a closed sentence. It then converts this sentence into clausal form and asserts each of the clauses into the . If 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 are true in the .

## Variables

 *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.

## Structures

 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.

## Builtin Logical Predicates

 = Logic (= ?x ?y). Unify ?x and ?y.

 Apply Logic (apply ). Apply lisp to , which may contain variables.

 Atom Logic (atom ). Succeed if is a lisp atom (not a list).

 Bagof Logic (bagof ). Try to solve . For each solution, collect into .

 Bagofn Logic (bagofn ). Try to solve . For up to solutions, collect into .

 Call Logic (call ). Try to solve .

 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 ). Bind with the result of evaluating lisp .

 Nonvar Logic (nonvar ). Succeed if is not an unbound logic variable.

 Numberp Logic (numberp ). Succeed if is a number.