Automated Reasoning Course

Part of the course Elective in Artificial Intelligence

Lecturer: Paolo Liberatore

2011/2012

News

Program

• Propositional logic
• Incomplete methods: GSAT and Unit propagation
• DPLL algorithm
• Propositional tableaux
• First-order logic tableaux: without and with unification
• Modal logics and tableau for modal logics
• LTL and model checking (labeling algorithm)
• Propositional and first-order natural deduction
• Hilbert proof systems
• Sequent calculus
• First-order logic resolution

Final tests

Oral test only; please email the professor for details.