THORN

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 (195,000 lines of OCAML and C++) and Prover9 (75,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. A short paper on THORN is available on Academia.

Trying It Out

The system is remarkably simple to use. Simply download, enter Shen, type (load "THORN 19.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]]. Remember to use lowercase symbols for functions and predicates.

Prolog Notation

THORN accepts Prolog notation treating capitalised terms as universally quantified variables; [all x [f x]] and [f X] are equivalent.

Procedural Attachment

Procedural attachment is a feature in theorem-provers going way back. For example, given as the goal 3 < 10, it is obvious that the native arithmetic engine needs to be called to prove this, not the inference engine itself. Procedural attachment is also a feature of Prolog.

After THORN 20, the higher-order call predicate in Shen Prolog can be invoked. For example in my Tarski-flavoured semantics I had an axiom.

[all x [all y [all z [[[name x] & [[copEng y] & [adjEng z]]] <=> [[istrueEng [cn x [cn y z]]] <=> [sat [den x] z]]]]]]

and

[adjEng "bald"]

But if I were to expand this system to incorporate thousands of English adjectives, I 'd have thousands of atomic statements in my axiom base. It would probably not compile; imagine a function def of adjEng with > 1 million loc!!

The solution is procedural attachment; I replace the axioms for adjectives by

[all x [[call [adjEng? x]] => [adjEng x]]]

and add

(defprolog adjEng?
X <-- (when (element? X (value *EngAdj*)));)

(set *EngAdj* ["bald" ....])

call, as you might know, figures in Shen Prolog. It calls a Prolog goal.

(prolog? (call (is X a)))
true

In THORN it is embedded in a way to preserve the syntax of the type prop.

The called procedure has access to resources from THORN; they are kept in the variables Prf, Max, Depth, Hyp. The most useful is the variable Hyp, which codes the hypotheses available at that stage of the proof. We can do stuff like this.

(define mytypechecking
-> [[all x [all type [[call [typecheck! x type (protect Hyp)]] => [x : type]]]]])

(defprolog typecheck!
X Type Hyp <-- (shen.system-S-h X Type Hyp);)

(kb-> (mytypechecking))
compiled
(<-kb [4 : number])

run time: 0.015625 secs
44 inferences, equality = false
depth = 20, complexity = -1, timeout = 60 secs
true

So you can link the type system into THORN. And that means, should you want to explore some exotic verification system or type theory, run under first-order logic and call on the Shen type system, you can do it.

One last caveat, call expects to know the arity of what it is calling. This is the higher-order magic behind the totally laconic definition of call in the kernel (the magic for this is in the kernel).

(define call
Call Bindings Lock Key Continuation -> (Call Bindings Lock Key Continuation))

So I use typecheck! to meet that need..

Some Proofs

There are some stored proofs returned by THORN here.

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.

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

1. The user enters (thorn.equality 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. (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.

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.

LATEST NEWS

The open Shen initiative. Hundreds of free online pages on Shen technology to appear in 2025.