Projects
"What I cannot create, I do not understand." — Richard Feynman
- Automated Theorem Provers
- SAT Solvers
- SMT Encodings
- Mathematical Proofs
- Model Checkers
- Formal Specifications
- Argument Maps
- Logic Programs
Build your own automated theorem provers
- Build Your Own First-Order Prover (Jens Otten / CADE 2019)
- How to Build an Automated Theorem Prover (Jens Otten / TABLEAUX 2019)
- Implementing First-Order Logic in Lean (Jeremy Avigad, Marijn Heule, & Wojciech Nawrocki)
- A Tutorial on Computational Classical Logic and the Sequent Calculus (Paul Downen)
Implement your own SAT solvers
- Understanding SAT by Implementing a Simple SAT Solver in Python (Sahand Saba)
- Writing a SAT Solver (Andrew Gibiansky)
- Decision Procedures for Propositional Logic: DPLL and CDCL (Jeremy Avigad et al. / Logic and Mechanized Reasoning)
Construct your own SMT encodings
- SAT/SMT by Example (Dennis Yurichev)
- Using SMT Solvers for Verification and Problem Solving (Jeremy Avigad et al. / Logic and Mechanized Reasoning)
- Strategies for SMT Solving in Z3: Python Tutorial (Z3 Community)
Formalize your own mathematical proofs
- The Natural Number Game (Kevin Buzzard & Mohammad Pedramfar)
- Mathematics in Lean (Jeremy Avigad & Patrick Massot)
- Logical Foundations: Software Foundations Volume 1 (Benjamin C. Pierce et al. / University of Pennsylvania)
Build your own model checkers
Write your own formal specifications
- Learn TLA+: Practical Formal Specification (Hillel Wayne)
- The TLA+ Video Course: Modeling and Checking State Machines (Leslie Lamport)
Diagram your own argument maps
- Diagramming Arguments (Lander University Philosophy Department)
- PhilMaps: Handy Hints for Argument Visualization (Simon Cullen / Princeton University)
- The Toulmin Argument Model (Purdue Online Writing Lab)