demodulation in theorem proving

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

Theorem proving is kind of a relaxation for me; like pigeon-shooting or drag racing except less violent or dangerous.  Exploding your theorem prover on a hard problems  and then figuring out how to change things is a fun challenge.

I've gone back to looking at Region Connection Calculus (RCC); a very simple first-order theory based on a single binary relation c meaning 'is connected to'.  The basic axioms are that A is connected to A and if A is connected to B then B is connected to A.   Everything else builds from this and the other ideas are based on definitions.  A is a part of B when everything connected to A is connected to B and so on.

Here is a function rcc which contains RCC.

(define rcc
  {--> symbol}
   -> (kb-> [
   [all x [c x x]]
    [all x [all y [[c x y] => [c y x]]]]   \\ loop detector needed!
    [all x [all y [[dc x y] <=> [~ [c x y]]]]]
    [all x [all y [[p x y] <=> [all z [[c z x] => [c z y]]]]]]
    [all x [all y [[pp x y] <=> [[p x y] & [~ [p y x]]]]]]
    [all x [all y [[eq x y] <=> [[p x y] & [p y x]]]]]
    [all x [all y [[o x y] <=> [exists z [[p z x] & [p z y]]]]]]
    [all x [all y [[po x y] <=> [[o x y] & [[~ [p x y]] & [~ [p y x]]]]]]]
    [all x [all y [[ec x y] <=> [[c x y] & [~ [o x y]]]]]]
    [all x [all y [[dr x y] <=> [~ [o x y]]]]]
    [all x [all y [[tpp x y] <=> [[pp x y] & [exists z [[ec z x] & [ec z y]]]]]]]
    [all x [all y [[ntpp x y] <=> [[pp x y] & [~ [exists z [[ec z x] & [ec z y]]]]]]]]
    [all x [all y [[ntpp-1 x y] <=> [nttp y x]]]]
    [all x [all y [[tpp-1 x y] <=> [ttp y x]]]]
    [all x [all y [[pp-1 x y] <=> [pp y x]]]]
    [all x [all y [[p-1 x y] <=> [p y x]]]]]))

Loads of theorems in this system.  Here is one

(<-kb [[[tpp a b] & [ec b c]] => [[dc a c] v [ec a c]]])

In THORN 10 I could not prove this, so in THORN 11 I added a loop detector
which coped with axiom 2 rather well.  

(<-kb [[[tpp a b] & [ec b c]] => [[dc a c] v [ec a c]]])
run time: 0.71875 secs
18640986 inferences
true

prf1.txt contains the proof of this theorem.

You notice that RCC mainly consists of equivalences which are really stipulative definitions.  Another alternative is to code these as rewrite rules and reduce all theorems

to one primitive relation c.  This was a technique, called demodulation, used by Woody Bledsoe in the 70s on set theory.  I gave this a go.

(4-) (rcc-prover [[[tpp a b] & [ec b c]] => [[dc a c] v [ec a c]]])
run time: 0.171875 secs
24586 inferences
true

The resulting proof (prf2.shen) is very long.  

There are about 36 problems in RCC of which THORN 11 solves about 6.  Whether demodulation fixes this I know not.

In theorem proving, you generally find that your latest gee whiz idea gets you a bit further down the road before the combinatorial explosion gets you.  This tantalising sense of almost there is one of the characteristics of the field.  As long as you take it recreationally, it is rather fun.

Mark

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

Now here is a doozy;

(6-) (prolog-memory 1e6)
1000000

You cannot do this in the default Prolog memory; you have to up it.

(7-) (rcc-prover [[[tpp x y] & [eq y z]] => [tpp x z]])
run time: 28.8125 secs
35590 inferences
true

This time indicates we are at the outer limits of search.    But only a few inferences

involved!  Why then the long time?  Well the proof is 14,300 lines long.  The demodulated

theorem - using only c - which says what my shorthand says, has 190 quantifiers in skolem

form.  I can't even attach the proof here which is > 90Mb.  Google refuses 

to accept it.

Mark

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

If I don't use demodulation and try the above theorem at depth 10; then THORN 11 fails

after 2.5 billion inferences and 4 minutes CPU time.

M.