Re: SPARK : surprising failure with implication

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 02 Jun 2010 09:56:23 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> (forall A,B in Boolean)
>>
>> not B => not A =
>>    = not not B or not A =
>>    = B or not A =
>>    = not A or B =
>>    = A => B
>>
> Yes, you confirmed that is right and so I'm not silly. But why Simplifier  
> do not seems to know it ? It is the basis of inference logic.

Modus ponens is, but in the form:

A => B, A
--------------
B

You have rather unusual:

A => B, not B
--------------------
not A

Disproving the antecedent from wrong consequent is not very common.

> That is why  
> I have such a weighty question in my mind : I wonder if I did something  
> wrong somewhere or if something is broken.
> 
> Do you have an idea ?

None, except that what looks obvious for a man is not for a computer and
conversely. (:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de