RCC - the power of controlled demoudulation

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

I promised I'd discuss how to crack RCC.  The key is to use demodulation instead of equivalences.  In THORN 6 this is done through lazy demodulation, in that the system does not demodulate everything at once to the primitive c - which would be awful to read - but demodulates by need.

The resulting proof of one RCC theorem is enormous.  However the time taken to compute is very short.   

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

run time: 0.015625 secs
25658 inferences
true

This problem originally crashed Shen Prolog and required prolog-memory to be reset to 1e6 from 1e4.  Then it computed as above.  The reason for the memory fault is that the proof is 11,134 lines long encapsulating 775 steps.   The proof does not use the reflexivity or symmetry axioms for c and I checked this against Prover9 which also does not use these rules in the production of the proof.

Mark

[Mark Tarver]

By a more optimal ordering of inference rules I've got the previous proof down to 6578 lines encompassing 519 steps.

However the proof of

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

run time: 0.125 secs
399764 inferences
true

takes 84,290 lines and 5503 steps.   I'll put THORN 6 up soon.

M.

--
You received this message because you are subscribed to a topic in the Google Groups "Shen" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/qilang/peaWqFNfzpA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/20d5ad5a-aeca-4063-b722-06457ebd6d7en%40googlegroups.com.

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

On Friday, 17 March 2023 at 22:37:56 UTC dr.mt...@gmail.com wrote:

By a more optimal ordering of inference rules I've got the previous proof down to 6578 lines encompassing 519 steps.

However the proof of

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

run time: 0.125 secs
399764 inferences
true

takes 84,290 lines and 5503 steps.   I'll put THORN 6 up soon.

(17-) (<-kb [[[tpp a b] & [tpp b c]] => [[tpp a c] v [ntpp a c]]])

run time: 0.03125 secs
206996 inferences

true 

Optimised now to  52,802 lines and 3,583 steps.

M.