Improving THORN: ways and means

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

Well, I'm planning my pilgrimage to Glastonbury and the summer hols.

But before I do, a word on THORN.  

THORN has it's limits, but one limit it does not have is a large program.  

At 580 loc, THORN is very lightweight.  It's fairly decent on FOL problems 

without equality; so-so on purely algebraic problems and quite bad on

theories that mix the two because of combinatorial problems.  Can it be bettered?

Roughly you can split improvements into 2x2 classes.

1.  Improvements that involved changing things inside THORN.

2.  Improvements that involve putting THORN within something outside THORN.

And this second division.

A.  Improvements that improve the compile time behaviour of THORN.

B.  Improvements that improve the run time behaviour of THORN.

1A. Includes all forms of equational unification.  2A. includes planners

and heuristic reasoners of all kinds.  1B. would include compilation

for parallel processing and 2B. perhaps combining THORN with 1B.

subsumption testing and maybe JIT compilation.  Personally I think 

2A. is likely to give the best fast returns.

Mark

[Woo]

Can THORN prove Perelman's theory about the shape of the universe and refused accept $1 million prize?

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

Probably not :).  THORN can prove some humanly unsolvable problems

like theorems from equivalential calculus that would defy any human

being to solve.   The leading example takes more than 4 million inferences

to solve and produces a proof of > 500 lines in seconds.  It can also find

proofs in Hilbert systems which I (not necessarily everybody) cannot find.

But in general THORN cannot do things that human mathematicians cannot.

However there is an experiment which I'm writing up to interface THORN to ChatGPT

which has yielded startling results and may change this picture.  

Mark

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

Said experiment is now up and readable.  In general, improvements to THORN

come from embedding it in a planner outside of it rather than tweaking the code

inside of it.  You can't really raise the bar on THORN itself very much.  But an

good planner can be awesomely effective.

M.

[Woo]

words fali me