|
THORN (Theorem prover based on HORN clause logic) is a program designed for solving problems in first-order logic
with equality. Download THORN and test problems here. The standard library is required to
run THORN.
THORN Itself
THORN is derived from Stickel’s PTTP and uses logic programming technology to achieve high inferencing
rates. The latest version is version 18. THORNt extends the PTTP from first-order logic to embrace first-order
logic with equality. THORN is not equivalent in problem-solving capability to systems with a larger code base
like Vampire and Prover9. Stickel’s observations apply to THORN.
Caveat: PTTP's high inference rate is achieved at the cost of not allowing more flexible search strategies or
elimination of redundancy in the search space by subsumption. Although PTTP is one of the fastest theorem provers
available when evaluated by its inference rate and performance on easy problems and it has been used to solve
reasoning problems in planning and natural-language-understanding systems effectively, its high inference rate
can be overwhelmed by its exponential search space and it is unsuitable for many difficult theorems.
Nevertheless THORN has solved some humanly unprovable theorems in equivalential calculus as well as Schubert's
Steamroller in 1 second under Shen/Scheme. The latter problem was unsolved by any ATP until 1984. It is also a small
program of around 530 lines of Shen, unlike Vampire (250,000 lines of OCAML and C++) and Prover9 (30,000 lines of C).
Unlike the PTTP, THORN uses a style of proof closer to natural deduction and the proofs are rather easier to read
than those from Vampire or Prover9.
THORN consists of two elements; a precursor program that is sound, complete and terminating for propositional calculus
and the main program which is based on logic programming technology. The precursor program can solve problems
independently of the logic programming component. If it fails to solve a problem, the decomposed problem is
handed to the logic programming component. I will write more on this.
Trying It Out
The system is remarkably simple to use. Simply download,
enter Shen, type (load "THORN 18.shen") w.o. type checking enabled and
(load "datatypes.shen") and switch on the type checker. Go to the folder
Problems and load any of the files there. There's lots of examples of
THORN propositions in that folder. BTW prop is a type in THORN. For any
successful run there is a file prf.txt in your home directory containing a proof.
Important Functions
The two important functions are kb-> (insert into the knowledge base) and <-kb (ask of the knowledge base).
The first takes a list of propositions (objects of the type prop) and compiles them into efficient code returning
compiled. The type of kb-> is (list prop) --> symbol.
<-kb receives a prop and tries to prove it returning either true (proved) or false (unproved) and placing a proof
in the file prf.txt in the home directory. The type of <-kb is prop --> boolean.
Loading the file loadme.shen in the THORN directory will load both THORN and the datatype definition of prop.
The Type prop
The sample files in the Problems directory contain numerous examples of propositions (props).
Here are the rules formally.
1. The logical constants are all, exists, =>, ~, <=>, &, v, =.
2. Any symbol which is not a logical constant is an (atomic) prop.
3. If P and Q are props, so is [~ P], [P => Q], [P v Q], [P <=> Q], [P & Q].
4. Any string, number, boolean, or symbol that is not a logical constant is a term.
5. A function symbol is any lowercase symbol that is not a logical constant.
6. A predicate is any lowercase symbol that is not a logical constant.
7. If f is a function symbol and t1 ...tn are terms then [f t1 ...tn] is a term.
8. If F is a predicate symbol and t1 ... tn are terms then [F t1 ...tn] is an (atomic) prop.
9. If t1 and t2 are terms [t1 = t2] is a prop.
10. If t1 and t2 are terms then [t1 : t2] is a prop.
10. If X is a lowercase symbol that is not a logical constant and P is a prop then [all X P] is a prop
and so is [exists X P].
11. If X is a lowercase symbol that is not a logical constant and t is a term and P is a prop
then [all X : t P] is a prop and so is [exists X : t P].
The expression [t1 : t2] is read as 't1 is of type t2' and [all X : T P] is a sugared form of [all X [[X : T] => P]].
Settings
Like the PTTP, 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 60 seconds. (thorn.timeout n) will set this to any desired number. There 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. By default
it is set to -1, which means there is no bound to complexity.
For equality, THORN uses a form of paramodulation. This is combinatorially explosive and by default it is
set to false. However it can be set to true by any of the following.
1. The user enters (thorn.paramod true).
2. The user enters a prop to kb-> containing the equality sign.
3. The user enter a prop to <-kb containing an equality sign.
(thorn.defaults) will reset all these settings to the default values.
Stuff in the Problems Folder
Simply loading any of the files in the Problems directory will run the problems in that file.
|
File | Contents |
|
ec.shen | Equivalential calculus axioms. These problems are impossible for humans. |
|
group.shen | Group theory which requires paramodulation. The same problem is submitted with unbounded and
differing levels of complexity. |
|
L.shen | A first-order formalisation of classical propositional calculus incorporating modus ponens and
three axiom schemas taken from Eliot Mendelson. The axiomatisation is in Prolog notation. |
|
pelletier.shen | A selection of propositional problems from Pelletier. |
|
schubert.shen | Schubert’s steamroller. |
|
set.shen | Basic set theory |
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.
THORN is not good at doing stand alone problems which do not require precompiled axioms. For instance,
entering (<-kb p) where p is a first-order theorem, may not issue in a proof in all cases.
If p is propositional, it will be proved. However if not, it may not be. The reason for this is that the
precursor program is a weak but terminating ATP that acts as a preprocessor for handing the problem to the
main program which works with compiled information. If this compiled information is absent, and the problem
is not solvable within propositional calculus, then the precursor
program will act alone and may fail to provide a proof.
As of June 2025, there is an odd bug about trying to perform an arithmetic operation on an unbound Prolog
variable which is hard to track down. It has occurred twice on different problems.
|
