LI2015: Sintaxis y semántica de la lógica proposicional

PorJosé A. Alonso

La clase de hoy del curso Lógica Informática ha tenido dos partes.

En la primera parte se ha presentado un panorama de la lógica y sus aplicaciones a la informática.

En la segunda parte se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

Finalmente, se ha iniciado el estudio de la semántica de la lógica proposicional como respuesta a la siguiente pregunta

  • ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?

Para responder la primera pregunta, empezamos definiendo, por recursión, el valor de verdad de una fórmula en una interpretación. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).

Hemos continuado planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.

Como tarea se ha propuesto resolver de los ejercicios 22 a 27 del capítulo 1 del libro de ejercicios (páginas 11 y 12).

Las transparencias de esta clase son las páginas 1-24 del tema 1.

I1M2015: Introducción a la programación funcional

PorJosé A. Alonso

En primera parte de la clase de hoy del curso de Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas y se ha mostrado el uso de Haskell y emacs (la sesión está grabada en este vídeo) y el proceso para la solución colaborativa de ejercicios (la sesión está grabada en este vídeo)

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

La segunda parte de la clase ha consistido en una introducción a la programación funcional basada en el tema 1. Se ha explicado

  • cómo definir y evaluar funciones en Haskell,
  • cómo comprobar propiedades de funciones en Haskell con QuickCheck,
  • cómo se resuelve un problema mediante programación imperativa y funcional,
  • los rasgos característicos de la progración funcional con Haskell,
  • los antecedentes históricos de Haskell y
  • cómo definir funciones mediante recursión y comprensión.

A lo largo del curso se profundizará en el estudio de los anteriores conceptos.

LI2015: Presentación del curso de “Lógica informática”

PorJosé A. Alonso

En la clase de hoy, se ha presentado el curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:

Reseña: A survey of interactive theorem proving

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titulado A survey of interactive theorem proving.

Su autor es Filip Marić (del Automated Reasoning GrOup (ARGO) en la Universidad de Belgrado, Serbia).

Su resumen es

Fully formally verified mathematics and software are long-standing aims that became practically realizable with modern computer tools. Reasoning can be reduced to several basic logical principles, and performed using specialized software, with significant automation. Although full automation is not possible, three main paradigms are represented in formal reasoning tools: (i) decision procedures for special classes of problems, (ii) complete, but potentially unterminating proof search, (iii) checking of proof-sketches given by a human user while automatically constructing simpler proof steps. In this paper, we present a survey of the third approach, embodied in modern interactive theorem provers (ITP), also called proof-assistants. These tools have been successfully developed for more than 40 years, and the current state-of-the-art tools have reached maturity needed to perform real-world large-scale formalizations of mathematics (e.g., Four-Color Theorem, Prime Number Theorem, and Feith-Thompson’s Odd Order theorem) and software correctness (e.g., substantial portions of operating systems and compilers have been verified). We discuss history of ITP, its logical foundations, main features of state-of-the-art systems, and give some details about the most prominent results in the field. We also summarize main results of the researchers from Serbia and personal results of the author.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Agda sobre metalógica titulado Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus.

Sus autores son Álvaro Tasistro, Ernesto Copello y Nora Szasz (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

In Substitution revisited, Alley Stoughton proposed a notion of (simultaneous) substitution for the Lambda calculus as formulated in its original syntax – i.e. with only one sort of symbols (names) for variables – and without identifying α-convertible terms. According to such formulation, the action of substitution on terms is defined by simple structural recursion and an interesting theory arises concerning the connection to α-conversion.

In this paper we present a formalisation of Stoughton’s work in Constructive Type Theory using the language Agda, which reaches up to the Substitution Lemma for α-conversion. The development has been quite inexpensive e.g. in labour cost, and we are able to formulate some improvements over the original presentation. For instance, our definition of α-conversion is just syntax directed and we prove it to be an equivalence relation in an easy way, whereas in Substitution revisited the latter was included as part of the definition and then proven to be equivalent to an only nearly structural definition as corollary of a lengthier development. As a result of this work we are inclined to assert that Stoughton’s is the right way to formulate the Lambda calculus in its original, conventional syntax and that it is a formulation amenable to fully formal treatment.

El trabajo se ha publicado en Electronic Notes in Theoretical Computer Science.

El código de las correspondientes teorías en Agda literario se encuentra aquí.