(no subject)

[gusl]

IMPS (An Interactive Mathematical Proof System), thanks to Freek Wiedijk for the reference!

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
dierence 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.

Comments

[perspectivism.livejournal.com]

Very very cool!

[gustavolacerda.livejournal.com]

I didn't know you were into this kind of thing.

[perspectivism.livejournal.com]

I'm into it theoretically -- one vantage point away, maybe! -- but not actively or professionally.

[gustavolacerda.livejournal.com]

interesting. Have you been following my other posts about this stuff, or did this one grab your attention to the subject?

Btw, this sort of idea could have applications in Law: e.g. making laws and contracts less ambiguous... applied to argumentation theory, such systems could force people to accept rational arguments. This is one of John McCarthy's dreams.

Assembly

[fare.livejournal.com]

I wonder if the mainstream of the Formal Mathematics community is using the analog of Assembly languages.
Indeed, lambda-calculus as used in LCF and its descendants (HOL, Coq, etc.) has been dubbed "The Assembly language of proof systems". That said, if you could give hints as to how IMPS does better, I'm all ears.

Re: Assembly

[gustavolacerda.livejournal.com]

Indeed, lambda-calculus as used in LCF and its descendants (HOL, Coq, etc.) has been dubbed "The Assembly language of proof systems".
by whom?

I don't know the system yet. The only idea I have is that it would be more natural to work in the language of the specific area... e.g. group theorists would like to work in the language of group theory, instead of in type theory. (I'm not sure though if this makes a significant difference to the group theorist)

This language is then translated (i.e. "faithfully interpreted") into the low-level language of the foundation (type theory, set theory, whatever).

I wonder if this is why current formalization work takes so damn long.

I'm just surprised that I hadn't heard of IMPS before. If it's that much better than the mainstream, people would be using it... so I wonder if there's a catch...

Btw, I've mentioned you in my revised proposal. http://student.science.uva.nl/~glacerda/FormalizingScienceIntuitively/
Comments are always welcome.

Re: Assembly

[selfishgene.livejournal.com]

I suspect the catch is, that it is still hard work to make worthwhile proofs, notwithstanding a good method of developing/describing them. (This statement is made after 30 seconds of analysis, so it may be total shit.)

[perspectivism.livejournal.com]

This post definitely grabbed my attention as the first software product (development environment) type approach I'd seen.

In general, I think I've noticed most of your posts touching on proofs & such -- but proof per se doesn't usually grab me. My main interest closest to proof might be how humans' automatic reasoning routines differ so much from proof-type logic!

I don't have much to do with Law nowadays, though I do still follow some Law&Econ writers.

[gustavolacerda.livejournal.com]

My main interest closest to proof might be how humans' automatic reasoning routines differ so much from proof-type logic!

This is also something I'm very interested in. I dream of working on investigating how people reason / make decision, and applying this knowledge to help actual people. Do you know Herbert Simon?


I don't have much to do with Law nowadays
Oh, what happened? Did you become a sort of life-improvement consultant? :-)