Reseña: Computational logic: its origins and applications

Lawrence C. Paulson publicó en 1998 el artículo Computational logic: its origins and applications cuyo resumen es

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the ‘logic for computable functions (LCF) approach’ pioneered by Robin Milner, where proofs can be constructed interactively or with the help of users’ code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

y su contenido es

  1. Introduction.
  2. A brief history of formal logic.
  3. Mechanized logic: the LCF tradition.
  4. A new theorem-proving architecture: Isabelle.
  5. Formalizing mathematics.
  6. Obstacles to formalizing mathematics.
  7. The way forward.

La Lógica en las ciencias computacionales

Se ha publicado un artículo sobre la enseñanza de la lógica titulado La Lógica en las ciencias computacionales.

Su autor es Edgar Serna M. (del Instituto Tecnológico Metropolitano, Medellín (Colombia)).

Su resumen es

En este trabajo se hace un análisis a la necesidad de incluir a la lógica en los procesos formativos en Ciencias Computacionales (CS por sus siglas en inglés). Se parte de un recorrido sobre la historia de la lógica en estas ciencias, posteriormente se describe la relación y la necesidad de incluirla en los procesos formativos relacionados, y al final se analiza qué, cuándo y qué tan profundo se debería trabajar en la formación en CS. Se trata de una revisión al estado del tema y a la importancia de incluirlo en los pregrados y en los posgrados en áreas de ciencias computacionales y tecnologías de información.

El artículo se ha publicado en la Revista Educación en Ingeniería.

LMF2013: Tableros semánticos en Haskell

En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de los tableros semánticos.

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa el módulo SintaxisSemantica desarrollado en la clase del día 27 de febrero.
Read More “LMF2013: Tableros semánticos en Haskell”

LMF2012: Ejercicios de sintaxis y semántica de la lógica proposicional en Haskell (2)

En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se han comentados las soluciones de los ejercicios de la 2ª relación, cuyo objetivo es la formalización de la sintaxis y la semántica de la lógica proposicional en Haskell.

Las soluciones de los ejercicios corregidos se muestran a continuación
Read More “LMF2012: Ejercicios de sintaxis y semántica de la lógica proposicional en Haskell (2)”

Lógica Computacional en Sevilla (30 años en una hora)

Ayer, en las Jornadas de Lógica, Computación e Inteligencia Artificial, hice una presentación sobre el desarrollo de la investigación de la Lógica computacional en la Universidad de Sevilla desde sus comienzos (en el Seminario de Lógica Matemática del curso 1980-81) hasta la actualidad.

El título de la presentación fue Lógica Computacional en Sevilla (30 años en una hora).

Las transparencias usadas en la presentación son las que se muestran a continuación

Descargar (PDF, 1.6MB)