Computational Logic

General characterization

Prerequisites

Available soon

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

Teaching method

There are two hours of theoretical classes and three 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 proplems 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 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.

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

Programs

Programs where the course is taught: