Lógica en Ciencias de la Computación (300CIG002)

 

Información Básica

  • Créditos: 3
  • Horas de Clase: 4 / semana
  • Horas de trabajo independiente: 5 / semana
  • Prerequisitos: Matemáticas Discretas para Computación (300MAG031)
  • Tipo de curso: Núcleo de Formación Fundamental.

Descripción del Curso

Logic provides the machinery needed to check whether a given argument follows from a given set of premises. It allows us to formally prove whether a statement is true or not.
Since the 19th century, logic has been stablished as the language of mathematics. It thus gives the rigour needed to perform mathematical proofs.
Logic is also of paramount importance for computer science and it has been called the calculus of computer science, i.e., it plays the same role that calculus plays for physical sciences and traditional engineering disciplines. For instance, the language of logic allows us to express, in a precise way, the specification of the system we want to built. Furthermore, logic provides mechanisms to (semi-automatically) prove if the proposed design and implementation satisfy the specification.

In this course we study the syntax, semantics and procedure definitions for propositional logic and first-order logic. With the help of tools such as COQ and Rodin, the student will apply his/her knowledge in the specification and verification of computer-based systems.

Objetivos

In the end of this course, the participants will be able to:

  1. Recognize the role of logic in mathematics and computer science.
  2. Translate statements from natural language into the language of Propositional Logic (PL)
    1. Define inductively the language of PL
    2. Establish and prove properties of well-formed sentences in PL
  3. Establish the truth of a sentence in PL
    1. Compute truth tables.
  4. Prove the validity of a sentence in PL
    1. Use a system for PL to prove the validity of formulas
    2. Prove be means of a theorem prover some tautologies in PL
    3. Prove by using resolution the validity of formulas
    4. Argue whether a system is sound and complete
  5. Specify properties by using the language of First Order Logic (FOL)
    1. Give meaning to FOL sentences
    2. Find a normal form for a given FOL formula
    3. Show the validity of a FOL formula
  6. Prove FOL formulas by using the sequent calculus
    1. Prove FOL formulas by using a theorem prover
    2. Identify some undecidable fragments of logic
  7. Relate computational steps and derivations in a proof
    1. Apply resolution in FOL to prove a given goal
    2. Write simple programs in (higher order) prolog.
  8. Specify and verify systems and program properties
    1. Specify properties of a given system or program
    2. Prove properties of a system with the aid of a theorem prover
    3. Identify other logical systems and their relation with computer science

Contenido

Topics marked with “*” are optional.

Chapter 1: Introduction

Sesión Horas de Clase Tópicos Bibliografía
1 1 Logic in Computer Science
1 1 Course rules and methodology

Total de Horas: 2.

Chapter 2: Syntax of Propositional logic (PL).

Sesión Horas de Clase Tópicos Bibliografía
2 2 The language of PL [1,Ch3] [2, Ch1] [3, Ch1]
3 4 Inductive proofs: Properties of the PL language [1,Ch3] [2, Ch1]

Total de Horas: 6.

Chapter 3: Semantics of Propositional logic (PL).

Sesión Horas de Clase Tópicos Bibliografía
5 2 Satisfiability, unsatisfiability and tautologies [1,Ch3] [2, Ch1] [3, Ch2]
6 2 Equivalences and Boolean algebras. [1,Ch3] [2, Ch1] [3, Ch2]

Total de Horas: 4.

Chapter 4: Decision procedures for Propositional logic (PL).

Sesión Horas de Clase Tópicos Bibliografía
7 4 Proof Theory: Sequents and proof systems à la Gentzen [1,Ch3] [3, Ch3]
8
9 2 Interactive proofs [4]
10 4 Resolution in PL and Complexity [1,Ch4] [2, Ch1] [3, Ch3]
11
12 2 Soundness and Completeness [1,Ch3]

Total de Horas: 12.

Chapter 5: Syntax and Semantics of First Order Logic (FOL).

Sesión Horas de Clase Tópicos Bibliografía
13 2 Signatures, terms and substitutions [1,Ch5] [2, Ch2] [3, Ch5]
14 2 Semantics: Structures and models [1,Ch5] [2, Ch2] [3, Ch5]
15 2 Satisfaction and validity [1,Ch5] [2, Ch2] [3, Ch5]
16 2 Normal forms [1,Ch5]

Total de Horas: 8.

Chapter 6: Proof Theory for First Order Logic (FOL).

Sesión Horas de Clase Tópicos Bibliografía
17 4 Proof Systems for FOL [1,Ch5] [2, Ch2] [3,Ch6]
18
19 4 Interactive Proofs [4]
20
21 2 Soundness and Completeness [1,Ch5] [3,Ch6]
22 2 Undecidability and incompleteness [1,Ch5] [3,Ch6]

Total de Horas: 12.

Chapter 8: Specification and Verification.

Sesión Horas de Clase Tópicos Bibliografía
23 2 Specification and properties [2, Ch4] [4, Ch9] [3, Ch9]
24 6 Specific theories and axioms: equality, sets , relations, functions, etc. [4, Ch9]
25
26

Total de Horas: 8.

Chapter 9: Logic as a Programming Language.

Sesión Horas de Clase Tópicos Bibliografía
27 2 Resolution in FOL [1,Ch8-Ch9] [3, Ch8]
28 6 Horn Clauses and PROLOG [1,Ch8-Ch9] [3, Ch8]
29
30

Total de Horas: 8.

Recursos

Bibliografía

  1. Jean Gallier. Logic For Computer Science: Foundations of Automatic Theorem Proving. June 2003. (This book is available at http://www.cis.upenn.edu/~jean/gbooks/logic.html).
  2. M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. 2004.
  3. M. Ben-Ari. Mathematical Logic for Computer Science. 2nd Edition. Springer. 2001.
  4. J-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
  5. Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer. 2004. (The french version is available here).
  6. D. Miller and G. Nadathur. Programming with Higher-Order Logic. Cambridge University Press. 2012.
  7. Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2001.

Instalaciones

Class room with video beam.

Material de este semestre