Learning Propositional Logic with Logic Programming
summary
Builds a runnable propositional-logic DSL in miniKanren embedded in Scheme, converts SL grammar into relations, and implements procedures to remove implications, push negations to negation-normal form, and produce conjunctive/disjunctive normal forms. Generates roughly 32 rewrite rules (duals and symmetries included), runs in a REPL-driven loop, and yields human-readable proof traces showing applied transformations. It works as a learning tool but can be slow via brute-force search and needs careful rule ordering for practical performance.
AI-written summary · about
chapters (9)
- 0:00Start
- 2:25Propositional Logic
- 10:07Compound Statements
- 16:13Compound Statement
- 21:30Normal Forms
- 30:00Implication Connective
- 32:04Remove the Implications
- 34:34Negation Normal Form
- 41:06Double Negation
related talks
43mProgrammation en Logique
43mAn Imperishable Wonderland of Infinite Fun
52mWhat logic can teach us, Scala programmers
01h 34mFormal Logic Undressed
22mCan Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
15mLogic Programming with Extensible Types (Lightning talk)
47mSemi-Automated Direction-Driven Functional Conversion
28mElements of Logic Programming in a Concatenative Functional Language