Jason (jcreed) wrote,

Finished chapter 2 of the copy of "Mechanizing Proof" that I borrowed from demoness101, which is shaping up to be a fantastic book. It's a bit disturbing to hear the same general ideas being spoken so long ago, and to realize they still haven't "won", but I guess a lot of particular progress has been made. Nonetheless, the whole endeavour of mechanical reasoning about mechanical systems needs to put its money and code where its mouth is pretty damn soon.

Frank is talking a bit in class about the stuff kitty_tape was working on last summer, with focusing and checking proofs in a format more human-friendly than λ-calculus terms. Also some neat stuff about abstract congruence closure algorithms. I need to go back and look at Mizar again.

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment