THORN

THORN (Theorem prover based on HORN clause logic) is a program designed for solving problems in first-order logic with equality. THORN is included in the Shen Library that comes with the kernel sources download (see the Download link above). It is loaded by request during installation. If you have not loaded it got to THORN in the directory Lib and type (load "datatype.shen") and (load "THORN20.shen"). The standard library is required to load and run THORN. If you want type checking remember to enter (include [prop term]).

Propositional Problems

The syntax for propositional calculus is:

1. A lowercase symbol on its own which is not a logical constant is a prop. The logical constants are ~, =>, <=>, &, v, all, exists, =

2. If P and Q are props so are [~ P], [P v Q], [P & Q], [P => Q], [P <=> Q]

The two basic functions for running THORN are kb-> (insert in knowledge base) and <-kb (prove from knowledge base) of types (list prop) --> symbol and prop --> boolean respectively. If the prop is provable then <-kb returns true. A proof is sent to the file prf.txt in the current directory.

THORN is sound, complete and terminating wrt propositional calculus. Hence any tautology will be proved by <-kb. The file Problems/pelletier.shen contains a number of them. e.g.

        
         (<-kb [[p => q] <=> [[~ q] => [~ p]]])  

         (<-kb [[~ [~ p]] => p])  

         (<-kb [[~ [p => q]] => [q => p]])

First Order Problems

We extend the syntax to first-order props.

3. If X and Y are symbols (other than logical constants), strings, booleans (true or false), or numbers then X and Y are terms. If F is a lowercase symbol (other than a logical constant) and X1 ... Xn are terms then [F X1 ...Xn] is a term.

4. If G is a lowercase symbol (other than a logical constant) and X1...Xn are terms then [G X1 ...Xn] is a prop.

5. If X and Y are terms then [X = Y] is a prop.

6. If P is a prop so are [all X P] and [exists X P] where X is a lowercase symbol other than a logical constant.

In the absence of props not asserted by kb->, THORN is sound, incomplete and terminating wrt quantificational and/or equality problems. In this context THORN functions as a weak first-order prover. It is more powerful when a list of props is submitted to kb-> as axioms. In this case THORN compiles the axioms into a Prolog program designed to solve queries posed wrt those axioms. In the Problems directory you will find many such files containing axioms for different systems.

kb-> accepts Prolog notation. Uppercase variables are allowed and read as universally quantified. So [f X] and [all x [f x]] are equivalent.

(kb-> [[all x [~ [m x e]]]
       [all x [all y [[[sub x y] & [sub y x]] <=> [=s x y]]]]
       [all x [all y [[sub x y] <=> [all z [[m z x] => [m z y]]]]]]
       [all x [all y [[pow x y] <=> [all z [[m z x] <=> [sub z y]]]]]]
       [all x [all y [[com x y] <=> [all z [[m z x] <=> [~ [m z y]]]]]]]
       [all x [all y [all z [[int x y z] <=> [all w [[m w x] <=> [[m w y] & [m w z]]]]]]]]
       [all x [all y [all z [[un x y z] <=> [all w [[m w x] <=> [[m w y] v [m w z]]]]]]]]])

The following are all provable.

(<-kb  [un a a a])  
(<-kb  [int a a a] )
(<-kb  [all x [all y [all z [[un x y z] <=> [un x z y]]]]])             
(<-kb  [all x [all y [[pow x y] => [m y x]]]])
(<-kb  [all x [all y [[pow x y] => [m e x]]]])
(<-kb  [all x [all y [[sub x y] <=> [un y x y]]]])
(<-kb  [[[com x y] & [com y z]] => [=s x z]])
(<-kb  [~ [com a a]])
(<-kb [[int a b c] => [[sub a b] & [sub a c]]])

Settings

THORN uses incrementally bounded depth first search up to a given maximum to seek solutions. The maximum is set by the user. (thorn.depth n) will set the depth which is by default 20. There is also a timeout which by default is 5 seconds. (thorn.timeout n) will set this to any desired number. There is a figure for controlling the complexity of the terms generated which means that any goal (an atomic prop which THORN is attempting to prove) whose terms collectively exceed this complexity will be axed from the search. (thorn.complex n) sets this. Complexity is measured by the length of the flattened list. By default it is set to -1, which means there is no bound to complexity.

THORN handles equality as two-way rewriting (see Academia again on this. THORN is not complete wrt equality. By default it is disabled and is enabled under the following conditions.

1. The user enters a prop to kb-> containing the equality sign.
2. The user enters a prop to <-kb containing an equality sign.

(thorn.defaults) will reset all these settings to the default values. (thorn.wipe-kb) will wipe the knowledge base.

Stuff in the Problems Folder

Simply loading any of the files in the Problems directory will run the problems in that file.

Some of the problems are commented out as too hard.

Issues

Beware that the predicates you use will be compiled into functions of the same name overwriting any defs of them which pre-exist. kb-> overwrites earlier axiom sets in that any any prop which uses a predicate F will overwrite the information about F in an earlier invocation of kb->. The timeout option seems a little liberal in its interpretation of time, giving the program more time to execute than allowed for.

Using the same predicate with a different arity in different contexts will cause problems. In case there is doubt whether a previous use of kb-> has done this (thorn.wipe-kb) will initialise the knowledge base.