release of FTP under THORN title

[dr.mt...@gmail.com]

I'm releasing the FTP under the title THORN (Theorem prover based on HORN clause logic).  THORN was the very first ATP I built as a novice in Franz Lisp which ran at the princely speed of 10 LIPS.   The other reason for the rename is that FTP confuses with file transfer protocol.    

I'm tinkering around with THORN 1.0 (= FTP 34.0)  because though it works it produces suboptimal proofs in certain cases.  The reason is that problems of the form (P & Q) are searched at a common depth, so that if P is solvable at depth m and Q at depth m+n the system will however search for a solution at m+n for both P and Q.   This may produce suboptimal proofs for P (proofs that are needlessly long).  I've fixed this and found that a 96 step proof shrinks to 55 steps.

However though good, this screws up the printing of the proof in THORN 1.0 so I'm fixing this before release.

Mark

[Joel McCracken]

here-to-fore I had always assumed here that when I saw FTP it was some news about changes to a FTP server, and ignored it; so I for one think this change is helpful for us ADHD-addled younger-people who have learned to apply crude filters to everything we see as a way to deal with the absolute deluge bombarding us on the internet every day. 

Making a mental note to check out THORN, see what it really is. It integrated now with Shen somehow, or does it still require another lisp to host it?

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/b66f1d97-b9c6-42b8-af0a-5ffd44d58f3fn%40googlegroups.com.

[dr.mt...@gmail.com]

THORN is totally Shen coded and relies on compilation to Prolog clauses for speed.  It tackles first-order logic without

equality and has an extension for equality.    I've just tested THORN 3 which produces a better proof for equivalential calculus

than THORN 1 (72 steps for THORN 3 vs 96 for THORN 1).  

THORN can do some problems that humans cannot but can't compete against systems like Prover9 and Vampire.

The main utility is that since it is coded in Shen, so it could be used as part of a verification system in Shen.  

THORN outputs proofs to a file automatically on success.

(set thorn.*depth* 13) \\ set depth of search to 13

(define mp
  {--> prop}
  -> [all x [all y [[[p [e x y]] & [p x]] => [p y]]]])      

(define yql
  {--> prop}
   -> [all x [all y [all z [p [e [e x y] [e [e z y] [e x z]]]]]]])

(define ec  
  {--> prop}
   -> [[[p [e x x]] & [p [e [e x y] [e y x]]]]
                               & [p [e [e x y] [e [e y z] [e x z]]]]])
                               
(kb-> [(mp) (yql)])   \\ assume these props in the knowledge base

(<-kb (ec))           \\ prove this conclusion

run time: 0.59375 secs
5980233 inferences
true

It's provable; output is in prf.txt

Attached is the proof.  

M.

[dr.mt...@gmail.com]

Also I think one advantage over Prover9 et al. is that the proofs are readable if you take the trouble.

As a uniform ATP THORN is very readable in its reasoning since it borrows from Prolog inferencing.

M.

[dr.mt...@gmail.com]

Also I should add - THORN is hackable - 588 lines vs Prover9 (28,000 lines) and Vampire (250,000 lines).

M.