verify_axioms_implications

[Radu Grigore]

Since I'm in spamming mode...

Classverification.verify_axioms_implications says in a comment that it
needs to check if
(a=>b) => (c=>d)
is valid, but the code computes
[a=>b] \/ ([c=>a] /\ [b=>d])
where [x] means "x is valid".

Is the comment right or the code?

regards,
radu

PS: Note that although ((a=>b) => (c=>d)) <=> (a=>b \/ (c=>a /\ b=>d))
is a tautology as the comment indicates, it is not the case that
[p]/\[q] is the same as [p/\q].

[Matthew Parkinson]

So this code is Stephan's.

I am hoping that it is a sound but not complete approximation. Stephan?

Matt

Sent from my iPhone

[Radu Grigore]

On Thu, Sep 9, 2010 at 9:53 AM, Stephan van Staden
<Stephan....@inf.ethz.ch> wrote:
> Chances are my code is wrong

Then I'll change it to one prover query and see if it breaks anything.

> - I [...] cannot see a counterexample
> showing that [p]/\[q] is not the same as [p/\q]. Did you intend to say that
> [p]\/[q] is not the same as [p\/q]?

Right, the disjunction is the problem (e.g. p="x is odd" and q="x is
even" in integers).

thanks,
radu

[Stephan van Staden]

Thanks! Please let me know if there are problems. S