ann: THORN 19 - the limits of technology

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

THORN 19 is up and with it the end of this line of development.  That doesn't mean there won't be a THORN 20,  It means that THORN cannot be persuaded to do better along the lines of its design.  The situation is a bit like that of the propeller-driven fighters at the end of WWII.  They really couldn't be persuaded to go faster because they had exploited the limits of piston-engined propeller-driven technology. We had some great planes like the Spitfire Mk XIV and the P-51D Mustang, but they were the end of the line.  A new technology was needed to take us through the sound barrier.

The barrier here is the combinatorial explosion which affects THORN and all uniform-method ATPs.  Optimisations are possible to improve performance.  These divide roughly into compile-time optimisations and run-time optimisations.   We've more or less run through compile-time optimisations.  Some run-time optimisations are impossible due to THORN's compiling away the axioms into hairy code for speed.  The local nature of Prolog search precludes others.   So you cannot push THORN much beyond where it is.

THORN will not beat big established ATPs like Vampire and Prover9, but it has some strengths.  The first is that, at 580 loc, it is much smaller than Vampire (250K loc) or Prover9 (30K loc).  So you can hack it.  And its written in Shen which is much clearer and more powerful than C++ or C like the preceding.

The second is that it actually produces nice proofs.   You can actually follow a THORN proof whereas the big systems I've mentioned produce almost unsurveyable proofs.

Third, THORN is actually not too bad at solving problems as long as you are cognisant of it's limits.  Bob Veroff, emeritus professor in ATP, has looked over a short paper on THORN and pronounced it 'novel and interesting' so I might write it up.

So could we do better and create a jet-powered THORN?  Something that combined THORN's awesome inference rate with directed intelligence.  What about a parallel THORN?

A parallel THORN without architectural changes would require a parallel Prolog.  This is something the Japanese failed to produce, though they tried in the Fifth Generation Initiative 40 years ago.   The prospects for a parallel THORN based on a parallel Shen Prolog are little better.  The use of destructive vector assignments in Shen Prolog and much else mitigates against parallel Prolog.  

A more promising line would be to compile the clauses separately into something like lambda functions and place these functions under some central control mechanism driven by some machine learning algorithm (neural net?).  This could be massively parallel production rule system and ramp up the inferences - maybe I could get to 100 MLips.  But the key lies in the intelligence and not the speed.

Mark

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

I just changed this download a little.  There was an error in the datatype

for prop which I corrected.  I also made external the type 'term'.   Both

'prop' and 'term' are now external to this package.  So you can enter 

[f a] : prop and a : term and be understood.

M.

[Woo]

"app1.shen" gives type error in rule 1 of appaxioms, and other problems give fn: thorn.mapf is undefined on windows

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

mapf is stlib.  That sounds as if you don't have the standard library loaded.

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.

You

You also need to load the datatypes folder that gives the type of prop. I noted my changes had introduced some errors, but that should be fixed now.

M.