At the end of this course, students will be able to:
- Recall and explain the syntax and semantics of Propositional Logic (PL) and First-Order Logic (FOL)
- Recall and explain the definition and use of Natural Deduction rules for reasoning within PL and FOL
- Construct Natural Deduction proofs for PL and FOL, and analyze the correctness of existing proofs
- Recall and construct proof terms to annotate PL proofs and interpret their correspondance to lambda calculus
- Recall and explain the syntax and semantics of Answer Set Programming (ASP)
- Model computational systems with ASP, apply model checking tools towards their verification
- Explain the correspondence between Horn-Clauses, its proof theory and Logic Programming
- Write ASP programs to solve simple programming problems and correlate their execution to proof construction