Computational Logic
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
General characterization
Code
7336
Credits
6.0
Responsible teacher
Carlos Augusto Isaac Piló Viegas Damásio, Ricardo João Rodrigues Gonçalves
Hours
Weekly - 5
Total - 66
Teaching language
Português
Prerequisites
N/A
Bibliography
A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Shawn Hedman. Oxford Texts in Logic, 2004.
Lógica Computacional: Proposicional e de 1ª ordem. Apontamentos de Paula Gouveia e F. Miguel Dionísio. Instituto Superior Técnico.
Logic in Computer Science: modelling and reasoning about systems.
Michael Huth and Mark Ryan.
Cambridge University Press, 2004.
Language Proof and Logic.
Jon Barwise and John Etchemendy.
CSLI Publications, 2003.
Teaching method
There are three hours of theoretical classes and two hours of laboratory classes per week.
In the theoretical classes, the fundamental concepts of computational logic are presented (namely propositional and first-order languages, interpretations and validity, coherent demonstration rules, coherent and complete proof systems), these concepts being illustrated with several examples and two formal systems: Natural Deduction closer to human reasoning and Resolution, more appropriate to computational implementation.
In the lab classes, students apply these concepts in several problems that are proposed to them, which, although simple, forces them to use the knowledge exposed in the theoretical classes and to consolidate their abstract and rigorous reasoning.
Evaluation method
The evaluation can be carried out through three tests, on dates to be indicated in CLIP, each one requiring prior registration. The tests are classified with a grade from 0 to 20 values, rounded to the first decimal place.
Alternatively, the assessment may be carried out through an exam (exame de recurso), on a date to be specified in CLIP.
Both the tests and the exam will be carried out in person, being without consultation, and the use of any electronic device is not allowed.
The final grade is obtained through:
1. Arithmetic average of the scores of the 3 tests, rounded to an integer, or
2. The grade of the exam (exame de recurso)
A student who has a final grade equal to or greater than 10 is approved.
Subject matter
Propositional Logic
Syntax:
inductive definition of propositional language
terms from natural language descriptions
Semantics:
truth tables
valoration and interpretation structure: satisfaction relation
validity and logical consequence; equivalence
Deductive system: natural deduction
introduction and elimination rules
derivations and proofs
correctness and completeness
Decision algorithm
Conjunctive normal form and clausal form
Resolution
First Order Logic
Syntax:
alphabet and first order language
terms from natural language descriptions
free variables and substitution
Semantics:
valoration and interpretation structure: satisfaction relation
validity and logical consequence; equivalence
Deductive system: natural deduction
Introduction and elimination rules
derivations and proofs
Correctness and completeness (sketch)
Decision algorithm
Skolemisation and unification
Resolution