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