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.

Integración Curricular

Resultados de Programa (ABET)

(A) La habilidad para aplicar conocimientos de matemáticas, ciencias e ingeniería.

(J) La habilidad para aplicar los fundamentos y principios de las matemáticas y de la computación en el modelamiento y diseño de sistemas computacionales de manera que se demuestre comprensión de las ventajas y desventajas en las decisiones de diseño.

(K) La habilidad para aplicar los principios de diseño y desarrollo de software en la construcción de sistemas de diferente complejidad.

Relevancia del curso con los resultados de programa

Resultados de Programa
A B C D E F G H I J K
Relevancia 3 3 3

Escala: (1) baja relevancia - (5) alta relevancia.

Integración de objetivos, contenido y metodología del curso

Resultados del Programa Indicadores de Desempeño Objetivos/Contenido del Curso Actividades de aprendizaje Instrumentos de medición
(A) Aplicación de Conocimientos (A1) Identificar los fundamentos científicos y los principios de ingeniería que rigen un proceso o sistema. (Conocimiento) (A2) Resolver problemas relacionados con la disciplina y otras áreas por medio de la utilización de conocimientos, modelos y formalismos de las ciencias de la computación, las matemáticas y la ingeniería. (Aplicación) All Lectures and assignments Exams and assignments
(J) Modelamiento y diseño de sistemas computacionales (J1) Reconocer la importancia del modelamiento cuando se resuelve un problema. (Compresión). (J2) Relacionar conceptos y principios teóricos para la resolución efectiva de un problema. (Síntesis). . (J3) Combinar principios de matemáticas, computación e ingeniería para modelar una situación. (Síntesis). All Lectures and assignments Exams and assignments (related to the specification and verification of programs and systems)
(K) Desarrollo de software (K3) Establecer invariantes y propiedades de componentes de software. (Análisis). . All Lectures and assignments Exams and assignments (related to the specification and verification of programs and systems)

Recomendaciones del Director del Programa

Reglas del curso

Calificación y Balance de Evaluación del Curso

Instrumento Porcentaje A J K
Exam I 25% 100%
Exam II 25% 30% 40% 40%
Exam III 25% 20% 40% 40%
Assignments 25% 50% 50%

Uso de material en exámenes

It is not allowed to use personal computers or mobile devices during exams.

Asistencia

Mandatory.

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

 
materias/laogica-cs.txt · Última modificación: 2013/11/08 11:28 por alexvalencia
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki