Automated Reasoning: Lessons

• Propositional logic
• Incomplete methods: GSAT and Unit propagation
• DPLL
• Propositional tableau
• First-order logic, examples
• First-order logic tableaux: ground and with unification
• Modal logics and tableau for modal logics
• LTL, model checking and symbolic model checking
• Propositional natural deduction and first-order natural deduction
• Hilbert proof systems
• Sequent calculus
• Resolution
• Proof complexity