LI2013: Semántica de la lógica proposicional

PorJosé A. Alonso

El objetivo fundamental de la clase de hoy del curso Lógica Informáticaha consistido en responder estas dos preguntas:

  • ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?
  • ¿cómo se puede construir un programa para que dada un conjunto de fórmulas S una fórmula F decida si es consecuencia de S?

Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursió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.

Además, se han definidos los conceptos de equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y la relación de consecuencia lógica.

Se ha visto la equivalencia de los siguientes problemas

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos.

También, se ha explicado cómo se puede usar en la resolución de los anteriores problemas el Gateway to Logic.

Finalmente, se han comentado las soluciones de la 2ª relación y cómo se puede usar APLI2 para comprobar la corrección de la formalización.

Las transparencias de esta clase son las páginas 14-34 del tema 1
Read More “LI2013: Semántica de la lógica proposicional”

Automation of mathematical induction as part of the history of logic

PorJosé A. Alonso

Se ha publicado un artículo sobre la historia del razonamiento automático titulado Automation of mathematical induction as part of the history of logic.

Sus autores son

Su resumen es

We review the history of the automation of mathematical induction.

This article is further organized as follows.

§§ 4 and 5 offer a self-contained reference for the readers who are not familiar with the field of mathematical induction and its automation. In § 4 we introduce the essentials of mathematical induction. In § 5 we have to become more formal regarding recursive function definitions, their consistency, termination, and induction templates and schemes.

The main part is § 6, where we present the historically most important systems in automated induction, and discuss the details of software systems for explicit induction, with a focus on the 1970s. After describing the application context in § 6.1, we describe the following Boyer–Moore theorem provers: the Pure LISP Theorem Prover (§ 6.2) Thm (§ 6.3) Nqthm (§ 6.4), and ACL2 (§ 6.5). The most noteworthy remaining explicit- induction systems are sketched in § 6.6.

Alternative approaches to the automation of induction that do not follow the paradigm of explicit induction are discussed in § 7.

After summarizing the lessons learned in § 8, we conclude with § 9.