You Didn't Know It, but You Really Want to Learn Sequent Calculus
summary
Shows an implemented sequent-calculus prover in Scala that reifies types to formulas via a ToFormula type class, uses Cats Show for readable output, and encodes rules (identity, implication right, pair/either handling) as data. The prover takes a sequence like A × B ⊢ A ∨ C, breaks it into subgoals, and produces a printed proof tree; typeclass-driven derivation supplies leaf converters. Code generation from proof to executable program remains unfinished, though proof extraction prints correctly. prover outputs proof trees
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:10Discovering Sequent Calculus
- 3:20Programming
- 10:35Example
- 12:35Type Class
- 16:10The Tough Part
- 16:40The Goal
- 17:30Proof
- 22:05Complex Formula
- 30:09Sequence
- 34:35Rules
related talks
52mWhat logic can teach us, Scala programmers
19mAutomated Verification of Fundamental Algebraic Laws
37mThe DOT Calculus: An Introduction for Scala Programmers
23mReasoning about types and code
52mType Theory and its Meaning Explanations
56mCalculating Intuitionistic Logic in Scala
01h 34mFormal Logic Undressed
42mLive-Coding Mathematics Your First Clojure Proof