Automated Reasoning Course

Part of the course Elective in Artificial Intelligence

Lecturer: Paolo Liberatore

2016/2017

Schedule

Thursday, 14-15:30, room A7

Program

The course presents the main methods for checking satisfiability or entailment of formulae in propositional logic, first order logic, and modal logics, including in particular the modal logics of time.

• Propositional logic
• Incomplete methods: GSAT and Unit propagation
• DPLL
• Propositional tableau
• 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

Final tests

Oral test only; please email the professor for details.