Projects
This page is a curated collection of well-written, step-by-step guides for learning Logic through hands-on, project-based practice.
What I cannot create, I do not understand — Richard Feynman.
These projects are meant to support learning throughout the curriculum, not only at the end.
By building, writing, creating, or reconstructing real artifacts in the field, learners develop practical understanding alongside theoretical study.
Tutorials
- Propositional Calculus
- First-Order Logic
- Modal Logic
- Proof System
- Natural Deduction System
- Sequent Calculus
- Tableau System
- Hilbert-style Axiomatic System
- Automated Theorem Prover
- Proof Assistant Kernel
- Logical Semantics
- Model Checker
- Logical Inference Engine
- Argument
- Formal Proof
Propositional Calculus
- Implementing Propositional Logic in Lean (syntax, semantics, basic procedures) (Online book chapter / code tutorial)
First-Order Logic
- Implementing First-Order Logic in Lean (syntax, semantics, unification) (Online book chapter / code tutorial)
- Build Your Own First-Order Prover tutorial series (CADE hands-on parts) (Slide-based tutorial / implementation guide)
Modal Logic
- How to Build Models for Modal Logic (Kripke structures walkthrough) (Video tutorial / model construction)
Proof System
- How to Build an Automated Theorem Prover (TABLEAUX tutorial series, covering calculi) (Slide-based tutorial / implementation guide)
Natural Deduction System
- How to do Natural Deduction Proofs (step-by-step rule application) (Video tutorial / proof construction)
Sequent Calculus
- A Tutorial on Computational Classical Logic and the Sequent Calculus (introduction to rules and structure) (PDF tutorial / conceptual build)
Tableau System
- How to Build an Automated Theorem Prover (includes tableau parts in sequent/tableau tutorial) (Slide-based tutorial / implementation guide)
Hilbert-style Axiomatic System
(No strong from-scratch procedural guides found; axiomatic systems are often presented descriptively.)
Automated Theorem Prover
- How (and why) to Build an Automated Theorem Prover (Java implementation walkthrough) (Video series / implementation)
- Build Your Own First-Order Prover (Prolog-based, hands-on) (Slide-based tutorial / code-focused)
Proof Assistant Kernel
- Implementing First-Order Logic in Lean (kernel-like syntax/semantics base, extendable) (Online book chapter / code tutorial)
Logical Semantics
- Implementing First-Order Logic in Lean (model semantics and evaluation) (Online book chapter / code tutorial)
Model Checker
- Build your own model checker in one month (tutorial overview, techniques survey) (Tutorial paper / construction guide)
Logical Inference Engine
- How to Build an Automated Theorem Prover (inference-focused implementation) (Video series / implementation)
Argument
- Diagramming Arguments (premise/conclusion structure, construction guide) (Online guide / argument building)
Formal Proof
- Natural Deduction Proofs: practise examples (step-by-step proof writing) (Video tutorial / proof construction)
- How to do Natural Deduction Proofs (rule-based formal proof building) (Video tutorial / proof construction)