Atp System Reference Manual

Contents

• Introduction
• Functions and Macros
• Variables
• Structures
• Builtin Logical Predicates

Introduction

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

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

Using ATP with Context Logic

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

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

Additional Notes

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

• <-
• ?-
• Add-Clause
• Add-Clauses
• Add-Fact
• Add-Facts
• Cl-Find
• Cl-Save
• Cl-To-Kif
• Clear-Predicate
• Deref-Exp
• Drop-Fact
• Drop-Facts
• Finds
• Finds-Cl
• Get-Clauses
• Id-Prove
• Install-Builtins
• Make-Kif-Kb
• Make-Prolog-Kb
• Prolog-Kb-All-Atoms
• Prove-All
• Tell-Cl
• Tell-Kif
• Top-Level-Prove

Variables

• *Ancestor-Cycle*
• *Ancestor-Reduction*
• *Ancestors*
• *Circularity*
• *Depth-Incr*
• *Depth-Max*
• *Depth-Start*
• *Inference-Count*
• *Occurs-Check*
• *Proof-Collect*
• *Search-Cut-Off*

Structures

• Kif-Kb
• Prolog-Kb

Builtin Logical Predicates

• =
• Apply
• Atom
• Bagof
• Bagofn
• Call
• Cut
• Is
• Nonvar
• Numberp
• Read
• Repeat
• Setof
• Test
• Unp
• Var
• Write

Functions And Macros

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

Variables

*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

Prolog-Kb		Structure
The structure that defines the atp kb.

Builtin Logical Predicates

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.