Lógica en Ciencias de la Computación

Información Básica

  • Código y Nombre: 300CIG002, Lógica en Ciencias de la Computación.
  • Créditos y horas de contacto: 3 Créditos, 4 horas por semana.
  • Nombre del profesor o coordinador del curso: Eduardo Tofiño.
  • Tipo de curso: Abierto.

Textos del Curso

  • 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).
  • M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press. 2004.
  • M. Ben-Ari. Mathematical Logic for Computer Science. 2nd Edition. Springer. 2001.
  • J-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
  • 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).
  • D. Miller and G. Nadathur. Programming with Higher-Order Logic. Cambridge University Press. 2012.
  • Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2001.

Información Específica 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 Específicos del Curso

Objetivos de aprendizaje:
  • Recognize the role of logic in mathematics and computer science.
  • Translate statements from natural language into the language of Propositional Logic (PL).
  • Establish the truth of a sentence in PL.
  • Prove the validity of a sentence in PL.
  • Specify properties by using the language of First Order Logic (FOL).
  • Prove FOL formulas by using the sequent calculus.
  • Relate computational steps and derivations in a proof.
  • Specify and verify systems and program properties.
Relación con los resultados de programa
Resultados de Programa
A B C D E F G H I J K
Relevancia 4 1 1

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

Tópicos del Curso

  • The language of PL
  • Inductive proofs: Properties of the PL language.
  • Satisfiability, unsatisfiability and tautologies.
  • Equivalences and Boolean algebras.
  • Proof Theory: Sequents and proof systems à la Gentzen.
  • Interactive proofs.
  • Resolution in PL and Complexity.
  • Soundness and Completeness.
  • Signatures, terms and substitutions.
  • Semantics: Structures and models.
  • Satisfaction and validity.
  • Normal forms.
  • Proof Systems for FOL.
  • Interactive Proofs.
  • Soundness and Completeness.
  • Undecidability and incompleteness.
  • Specification and properties.
  • Specific theories and axioms: equality, sets , relations, functions, etc.
  • Resolution in FOL.
  • Horn Clauses and PROLOG.
 
pregrados/dptoccomputacionyelectronica/logica.txt · Última modificación: 2014/07/15 16:05 por lsosorio
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki