FTP 36 beats Prover 9 on region connection calculus

[Mark Tarver]

For aficionados of automated reasoning, Prover 9 is the lineal descendent of OTTER which was until the early years of this century, the best automated theorem prover in the world.  The title is now held by Vampire in Manchester.

Region connection calculus is a first-order theory covered in https://en.wikipedia.org/wiki/Region_connection_calculus.  I'm running FTP 36 under Bruno's Shen/Scheme port.   The axioms are entered as definitions.

      [[all x [c x x]]
       [all x [all y [[c x y] => [c y x]]]]
       [[dc X Y] =df [~ [c X Y]]]
       [[p X Y] =df [all z [[c z X] => [c z Y]]]]
       [[pp X Y] =df [[p X Y] & [~ [p Y X]]]]
       [[e X Y] =df [[p X Y] & [p Y X]]]
       [[o X Y] =df [exists z [[p z X] & [p z Y]]]]
       [[po X Y] =df [[o X Y] & [[~ [p X Y]] & [~ [p Y X]]]]]
       [[ec X Y] =df [[c X Y] & [~ [o X Y]]]]
       [[dr X Y] =df [~ [o X Y]]]
       [[tpp X Y] =df [[pp X Y] & [exists z [[ec z X] & [ec z Y]]]]]
       [[ntpp X Y] =df [[pp X Y] & [~ [exists z [[ec z X] & [ec z Y]]]]]]]

The theorem to prove is:

[[[tpp a b] & [ec b c]] => [[dc a c] v [ec a c]]]

The resulting proof was gained in 0.062 seconds and is 439 steps long and 5,442 lines long and takes 29,028 inferences to secure.  It's too large to paste into this message, so I'm attaching it to this email.

Prover 9 gets a proof in 0.49 seconds; meaning FTP is running at 8X faster in terms of arriving at a solution.   So we've actually graduated out of the minor leagues into the major.

Prover 9 is ballpark about 30,000 lines of C vs FTP 36 which is currently 634 lines of Shen.

It's a good result so I'm going to bed.

Mark

[Mark Tarver]

FTP 37 - an optimised version of FTP 36 gets the same result in 16,039 inferences

compared to 29,028 inferences of FTP 36.

Mark