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)

    More things to add to the "chord progressions that aren't cliches-I-already-know-about nonetheless covertly appearing in multiple places" file.…

  • (no subject)

    Consider the chord motion in Lights's "Cactus In The Valley" that happens around 49s in: v link goes here | F G C C | F G C C | F G Am D7 | F G…

  • (no subject)

    Cute little synth widget playground: https://blokdust.com/

  • 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