From: Paolo Capriotti <p.capriotti@...>
Date: 2005-07-08T11:39:50+09:00
Subject: Re: [SUMMARY] Inference Engine (#37)

> You can see that this class is always monitoring for a @contradiction in each of
> these methods.  However, I don't think this ever comes into play, since each
> assertion is tested before it's added.  (Correct me if I'm wrong Paulo!)

Yes, if no assertion is added when the opposite is already in the
graph after a deduction, one is granted not to obtain contradictions
on successive deductions.
This follows from the fact that (after the deduce method has been
called) the assertions form a theory which satisfies the following
property:
every theorem of either of the forms a -> b, not (a -> b) is an axiom.
This is not difficult to prove. One can use, for instance, boolean
ring theory and the Stone theorem.

Paolo