Computational Logic
Code
7336
Academic unit
Faculdade de Ciências e Tecnologia
Department
Departamento de Informática
Credits
6.0
Teacher in charge
Pedro Manuel Corrêa Calvente Barahona
Weekly hours
5
Total hours
66
Teaching language
Português
Objectives
Knowledge
- Syntax and semantics of propositional and first-order logic
- Resolution methods for propositional and first-order logic
- Natural deduction systems for propositional and first-order logic
Skills
- Specification logical formulae from descriptions in natural language
- Assessment of the logical validity of formulae, semantically, axiomatically, and syntactically
- Use resolution algorithms to establish the logical validity of formulae
Competences
- Ability of abstract and rigorous reasoning
- Ability of manipulating formal structures
- Learn to learn
Subject matter
1. Propositional Logic
1.1. Syntax:
• Inductive definition of propositional language
1.2.Semantics:
• Truth tables and Boolean algebra
• Valoration and interpretation structure: satisfaction
1.3 Deductive systems and Decision Algorithms
• Natural deduction: Introduction and elimination rules
• Resolution: Clausal form, Horn algorithm
2. First Order Logic
2.1. Syntax:
• Alphabet and first order language
• Terms from natural language descriptions
• Free variables and substitution
2.2. Semantics:
• Valoration and interpretation structure: satisfaction relation
2.3. Deductive systems and Decision Algorithms
• Natural deduction: Introduction and elimination rules
• Resolution: Clausal form, Skolemisation, Unification
3. Mathematical Induction
Bibliography
Main textbook:
• Language, Proof, and Logic, David Barker-Plummer, Jon Barwise, John Etchemendy, Center for the Study of Language and Information; 2nd edition, October 2011.
Additional reading:
• Mathematical Logic: a course with exercices. Part I: propositional calculus, boolean algebras, predicate calculus, René Cori e Daniel Lascar, Oxford Press, 2007.
• A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity, Shawn Hedman, Oxford Texts in Logic, 2004.
• Logic in Computer Science: modelling and reasoning about systems (2nd edition), Michael Huth and Mark Ryan, Cambridge University Press, 2004
Evaluation method
The assessment of this course is done by means of 4 tests, each with one hour duration, or through a final exam. The 1st and 2nd tests basically cover Propositional Logic whereas the 3rd and 4th cover First-Order Logic and Mathematical induction.
• Approval
Students obtaining a positive grade (Nac >= 10) in the continuous assessment, also obtain approval to the course with this grade, computed as the average of the marks obtained in each of the 4 tests (marked in a 0-20 scale) .
Nac = (T1+T2+T3+T4)/4.
• Exam
Students that did not obtain approval in the continuous assessment is admitted to a final exam, structured in 4 groups corresponding to the 4 tests, each group marked in a 0-20 scale. In this case, the final mark (Nf) is the average of the maximum grade obtained in each test/group.
Nf = (max(T1,G1)+max(T2,G2)+max(T3,G3)+max(T4,G4)) / 4
• Improvement
Students already approved in this edition of the course but wishing to improve their mark in the final exam will have a final mark, Nm, obtained similarly
Nm = (max(T1,G1)+max(T2,G2)+max(T3,G3)+max(T4,G4)) / 4
Students approved in previous editions of the course, may improve their previous mark through the final exam, obtaining a final mark, Nm, that is the maximum of the previous mark and that obtained in the exam.
Nm = max(Na, (T1+T2+T3+T4)/4 )
• Access to Exam.
There are no preconditions to be admitted to the final exam, all registered students have access to it.