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 Linear Temporal Logic (LTL) and its relation with finite state machines**Model**computational systems with finite state machines,**construct**LTL specifications for their behavior and**apply**model checking tools towards their verification**Explain**the correspondence between Horn-Clauses, its proof theory and Logic Programming**Write**Prolog programs to solve simple programming problems and**correlate**their execution to proof construction**Recall**and**explain**basic principles of nonmonotonic logic and default logic systems.