35 views

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

true

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

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

Sep 13, 2023, 10:54:12 AMSep 13

to Shen

Now here is a doozy;

(6-) (prolog-memory 1e6)

1000000

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

(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

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.

M.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu