THORN


 

 

THORN (Theorem prover based on HORN clause logic) is a program designed for solving problems in first-order logic with equality. It is derived from Stickel’s PTTP and uses logic programming technology to achieve high inferencing rates. 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.

THORN consists of two elements; a precursor program that is complete 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.

Requirements

The standard library is required.

Commands

The type prop of first-order formulae is defined. The sample files contain numerous examples of these formulae. The function kb-> of type (list prop) --> symbol compiles a list of props into code and returns compiled.

The function <-kb of type prop --> boolean receives a prop and returns true if it can prove it and false otherwise. Non-termination is a possibility. Note Prolog notation is accepted in kb->; [f X] is an acceptable form of [all x [f x]].

Any successful attempt has the proof echoed to prf.txt in the home directory.

There are two settings contained in three global variables.

thorn.*depth* takes a positive integer which sets the maximum depth of the search.

thorn.*paramodulate?* takes a boolean which if true allows paramodulation. This is needed to solve problems using equality.

The function (thorn.defaults) sets the defaults which are 20 and false respectively.

Syntax

1. The logical constants are all, exists, =>, ~, <=>, &, v.
2. The prefix eq is the identity sign.
3. Any symbol which is not a logical constant is an (atomic) prop.
4. If P and Q are props, so is [~ P], [P => Q], [P v Q], [P <=> Q], [P & Q].
5. Any string, number, boolean, or symbol that is not a logical constant is a term.
6. A function symbol is any lowercase symbol that is not a logical constant.
7. A predicate is any lowercase symbol that is not a logical constant.
8. If f is a function symbol and t1 ...tn are terms then [f t1 ...tn] is a term.
9. If F is a predicate symbol and t1 ... tn are terms then [F t1 ...tn] is an (atomic) 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].

See the sample files below for examples.

Inference rules

Rule Abbreviation Function
Reverse Skolemisation revsk reverse skolemises a conclusion, applied once at the beginning of every proof.
By Hypothesis hyp proves P when P is an assumption
Contradiction contradiction proves P given Q and [~ Q] as assumptions.
Associativity of disjunction assocv given [[P v Q] v R] to prove, convert to [P v [Q v R]]
Supposition supp given [P v Q] to prove assumes the complement P* and proves Q. P*, the supposition, has all free variables bound by universal quantifiers (universal closure).
& right &R given [P & Q] to prove, proves P and then Q.
Exists right eR given [exists X P] to prove replace it by Q where Q is the result of replacing all free occurences of X in P by a fresh variable Y.
Paramodulation paramodulation does paramodulation, given P as conclusion and X = Y <-- Q as an assumption replaces one occurrence of X by Y in P provided Q is provable.
Indirect chaining P <-- Q1 ... Qn given P to prove, try and prove Q1 ... Qn ; [~ P] is assumed. This is a combination of indirect proof and backward chaining.

Test Programs

There are a number of test programs which can be run. Each file can be loaded into Shen after the THORN is loaded. Problems will be automatically run when loaded.

File Contents
ec.shen Equivalential calculus axioms. These problems are impossible for humans.
group.shen Two theories from algebra - specifically group theory which require paramodulation.
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 problems from Pelletier.
schubert.shen Schubert’s steamroller.
set.shen Basic set theory

Download

Download THORN and test problems here.

LATEST NEWS

The support page for the text Logic, Proof and Computation is established.

______________________________

THORN Theorem prover derived from HORN clause logic is available.

______________________________

Shen Education Channel starts on Youtube.

______________________________

Yggdrasil project launched - the grand unification of programming languages.

______________________________

Want to advertise on this site? Go to the contacts page.

Built by Shen Technology (c) Mark Tarver, September 2021