(no subject)
Dec. 20th, 2004 06:46 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslIMPS (An Interactive Mathematical Proof System), thanks to Freek Wiedijk for the reference!
This is exactly what I've been asking for... not only does it provide interpretations, but it's also interactive. High-level proving.
I wonder if the mainstream of the Formal Mathematics community is using the analog of Assembly languages.
In contrast to the formal proofs described in logic textbooks,
imps proofs are a blend of computation and high-level inference. Consequently,
they resemble intelligible informal proofs, but unlike informal
proofs, all the details of an imps proof are machine checked. imps emphasizes
interactive proof development. There is essentially no structural
di erence between completed proofs and partial proof attempts.
This is exactly what I've been asking for... not only does it provide interpretations, but it's also interactive. High-level proving.
I wonder if the mainstream of the Formal Mathematics community is using the analog of Assembly languages.