Propositional logic and satisfiability

Classical propositional logic: truth-table semantics, natural deduction and its completeness, functional completeness, normal forms and CNF transformations, resolution, interpolation, SAT-solving procedures (Davis–Putnam, DPLL, 2-SAT, Horn-SAT) and binary decision diagrams.

• Propositional natural deduction
• Binary decision diagrams
• Conjunctive normal form
• Craig interpolation
• DPLL algorithm
• Functional completeness
• Horn satisfiability
• Model-count-preserving CNF transformations
• Resolution
• 2-satisfiability
• Davis–Putnam algorithm
• Tseitin transformation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.