Fundamentos de Lógica e Teoria da Computação

Objectives

Understand proof theory for first-order logic theories. Learn techniques for proving quantifier elimination and decidability of theories. Learn about combination of first-order theories and preservation results for decidability.

Syllabus

Reasoning with first-order theories. Gentzen calculus. Soundness and completeness using Hintikka sets. Cut elimination and Craig interpolation. Sufficient conditions for the decidability of a theory: computable quantifier elimination, reduction, completeness, quantifer elimination and categoricity. Elimination of quantifiers: symbolic and via algebraically prime models and existence embeddings, proto-adjunction and iteration. Combination of first- order theories: preservation of satisfiability and decidability.

Cross Competence Component

The UC allows the development of transversal competences on Critical Thinking, Creativity and Problem Solving Strategies, in class, in autonomous work and in the several evaluation components. The percentage of the final grade associated with these competences should be around 15%.