Re: [isabelle] Announcement: Isabelle/HOLF



Hallo,

I thought I should maybe reply to these questions since it was me who
wrote most of exfalso:


> 1) I'm really missing sledgehammer. I have a problem to prove the
> following theorem, which is an old challenge problem from a leading CPU
> manufacturer:
>   theorem fpu_correct: "1.0 + 1.0 = 3.0" 
>
> Due to my understanding, the Falso-Logic should be able to prove it.
> However, when I tried sledgehammer, it does not find a proof? Any hints?

My intuition tells me that exfalso should work fine on propositions like
that; I cannot guarantee that it will always work, but in this instance,
it works fine. Personally, I think the possibilities of application of
the exfalso prover in circuit verification are virtually unlimited, but
I'm hardly an expert in this area.

The integration with sledgehammer is a known issue; remember, this is
still merely a prototype and we did not put too much effort into getting
it to work with Sledgehammer. I don't know where the problem is here,
but unlike some other projects, we actually have a bug tracker, so you
may want to file a bug report about this:
https://github.com/larsrh/hol-falso/issues



> 2) For some really nasty Isabelle-Hacking, that I do not dare to
> reproduce on this list, a lemma of the following form would be nice:
>   lemma: "PROP P"

The purpose of the exfalso prover is mainly to extend and, in the long
run, replace certain older and somewhat slow and unreliable methods like
"blast" and "auto"; therefore, like these methods, it was not designed
to handle "prop" values. However, if you have an idea how to integrate
something like that into exfalso, do tell us, or better still, feel free
to fork the repository on Github and send us a pull request once you're
done.


Cheers,
Manuel





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.