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
• 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
• 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.)
• 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
• How to write a great Research paper