Jason (jcreed) wrote,
Jason
jcreed

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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments