Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Lecture
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
This lecture introduces a proof system for propositional formulas with decision and simplification, focusing on the case analysis rule and propositional resolution. The instructor explains the soundness of the proof system and demonstrates example derivations. The lecture covers simplification rules, unsatisfiability proofs, soundness consequences, refutation completeness, and resolution on clauses as a proof system. It also discusses conjunctive form, literals, clauses, and resolution as transitivity of implication. Exercises on using resolution to prove formula validity and unsatisfiability are included, along with unit resolution concepts.