Learn computational logic

Free, interactive tools, with no account and your progress kept in your browser.

• Learn Davis-Putnam SAT

  The Davis-Putnam (DPLL) algorithm for the Boolean satisfiability problem: every unit propagation, branch and conflict, step by step.

  Open tool →

• Learn Natural Deduction

  Natural deduction proofs in Fitch notation, for propositional logic: a line-by-line editor, generated proofs explained step by step, a lesson and exercises.

  Open tool →