u/dharmatechin r/ProgrammingLanguages • Recommends
Proof of ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) with Lean
0:00 / 0:00
#lean#theoremprover#propositionallogic
Proof of ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) with Lean
Eduardo Cavazos
149 subscribers • 2 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Eduardo Cavazos
Intermediate. Assumes working knowledge.
4.8K views6 years ago1 recommendation
Computer scienceProgramming languagesFormal methods and verificationComputation and complexity
Eduardo Cavazos demonstrates how to prove a propositional logic equivalence using the Lean theorem prover.
Example from 3.6 of Theorem Proving in Lean: leanprover.github.io/theorem_proving_in_lean/propositions_an…Why it's here
1 person recommends thisWhat people say. Recommended as a practical example of writing propositional proofs in Lean.