Subject: Computational Logic

Scientific Area:

Mathematics

Workload:

80 Hours

Number of ECTS:

7,5 ECTS

Language:

Portuguese

Overall objectives:

1 - To introduce the basic theoretical concepts concerning logical reasoning and logical systems. To present several deductive systems both for propositional logic and to predicate logic. To expose the interrelation between the semantics and the deductive systems associated to those two logical systems.
2 - To highlight the interrelation between formal logic and computation (namely by presenting a programming language (Prolog) which uses the concept of logical deduction as its computation engine).

Syllabus:

1 - Propositional Logic (Propositional Calculus).
1.1 - The notion of formal (logical) system: language, semantics and deductive system.
1.2 - The language(s) of propositional calculus.
1.3 - An application of the principle of structural induction in propositional logic.
1.4 - Semantics of propositional calculus (truth tables, tautologies, the notion of logical consequence, normal forms; adequate sets of connectives).
1.5 - An axiomatization for the propositional calculus (proofs and derivations, the deduction theorem, soundness, consistency and adequacy/completeness of the axiomatization).
1.6 - Other deductive systems for propositional calculus.
2 - First-Order Logic (Predicate Calculus).
2.1 - First-Order Languages and their semantics (free term for a variable in a formula; instance of a tautology; interpretation, valuation and validity).
2.2 - An axiomatization for the predicate calculus (its soundness and consistency; the deduction theorem; adequacy/completeness of the proposed axiomatization).
2.3 - Another deductive system for predicate calculus.
3 - Introduction to Prolog.
3.1 - The logic programming paradigm.
3.2 - Introduction to Programming in Prolog.

Literature/Sources:

Hamilton, A.G. , 1988 , Logic for Mathematicians , Cambridge University Press
E. Mendelson , 1997 , Introduction to Mathematical Logic , Chapman & Hall
J. H. Gallier , 1986 , Logic For Computer Science: Foundations of Automatic Theorem Proving , John Wiley & Sons
Reis, M.D.L. , 2014 , Folhas de apoio às aulas de lógica computacional , Universidade da Madeira
Makinson, D. , 2012 , Sets, Logic and Maths for Computing , Springer
Martins, J. P. , 2014 , Lógica e Raciocínio , College Publications
U. Nilsson and J. Maluszynski , 1995 , Logic, Programming and Prolog , John Wiley & Sons Ltd.
Blackburn, P. & Bos, J. & Striegnitz, K. , 2006 , Learn Prolog Now! , College Publications
Carmo, J. & Gouveia, P. & Dionísio, F. M. , 2013 , Elementos de Matemática Discreta , College Publications
Fitting, M. , 1996 , First-Order Logic and Automated Theorem Proving , Springer
Gabbay, D.M. , 2007 , Logic for Artificial Intelligence and Information Technology , King's College Publications
Oliveira, A. J. F. , 1980 , Lógica Elementar , AEFCL
Oliveira, A. J. F. , 1981 , Teoria dos Conjuntos: Indutiva e Axiomática (ZFC) , Livraria Escolar Editora
Oliveira, A.J.F. , 2010 , Lógica & Aritmética: Uma introdução à lógica, matemática e computacional , Gradiva
Sterling, L. & Shapiro, E. , 1986 , The Art of PROLOG: Advanced Programming Techniques , MIT Press

Assesssment methods and criteria:

Classification Type: Quantitativa (0-20)

Evaluation Methodology:
Teaching Methodologies: Theoretical expository lectures; Practical problem solving classes; Classes devoted to practical laboratory work involving the use of Prolog. Assessment Methodologies: The assessment is made by means of one of the two following sets of evaluation elements (to be determined by the professor responsible for the course at the beginning of the semester): (i) Two compulsory written tests and an assignment, with the following weight distribution in the final grade: First test: 40%; Second test: 45%; Assignment: 15%. (ii) Two compulsory written tests and a mini-test, with the following weight distribution in the final grade: First test: 40%; Second test: 40%; Assignment: 20%.