Enrichment & Ancillary
- Why we study proofs
- Formal Methods Successes and Directions
- Specifying Properties on Pure Functions
- Mob Programming, at a distance
- An introduction to the ACL2 theorem prover
- Suggested links and help for steering ACL2
- Annotated ACL2 Examples
- Milestones from the 70s to ACL2
- Design Goals of ACL2
- Just what is the ACL2s sedan?
- Defdata in ACL2s
- More on the Ackermann Function + History
- Boolean Reasoning in ACL2 From the documentation.
- Results of the SAT Solver Competition at the 2018 Computational Logic Olympic Games
- SAT/SMT by Example As it suggests, scores of examples. Also a good place to start. SAT != SMT.
- CNF, DNF Normalization, Visualized
- Zhegalkin polynomials
- Quine-McCluskey Algorithm, Visualized
- It’s tough to organize a pub crawl
- A Profile of Mathematical Logic (A fun, quick-ish read on the story of modern logic)
- The Search for Mathematical Roots, 1870-1940: Logics, Set Theories and the Foundations of Mathematics from Cantor through Russell to Gödel (A grown-up text on much of the same.)
- A Modern Program Synthesis Survey
- Philosophy of Computer Science (Draft text)
- Logicomix (It’s a comic about Russell and early 20th century mathematical logic. ᕕ( ᐛ )ᕗ)
- An Introduction to Non-classical Logic (The conditional beyond the material)
- The Craft of Scientific Writing E-Book available via NEU library.
- Advice on Structure and Content
- SPJ Advice on how to write a research paper
- How to write a great Research paper
- Keeping logic in the trivium of computer science: a teaching perspective
- Pfenning’s Lecture notes on the Curry-Howard isomorphism
miniKanren constraint systems
- Slides
- “Gentle introduction to SMT” Video
- Constraint solvers for the working PL researcher
- Theorem provers are a PL researcher’s best friend
- Pseudo-boolean constraints
-
Chiang’s short story “Seventy-two Letters” (Audio version)
- Chiang’s “Division by Zero” (a story about ex-falso quodlibet)
- Russell’s “The Metaphysician’s Nightmare” (a story about the troubles with negation).