demodulation in theorem proving

Skip to first unread message

Sep 13, 2023, 10:19:31 AMSep 13
to Shen
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

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

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.



Sep 13, 2023, 10:54:12 AMSep 13
to Shen
Now here is a doozy;

(6-) (prolog-memory 1e6)

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

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.


Sep 13, 2023, 11:02:23 AMSep 13
to Shen
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.


Reply all
Reply to author
0 new messages