LMF2019: Sintaxis y semántica de la lógica de primer orden

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado la sintaxis y la semántica de la lógica de primer orden como respuestas a las siguientes preguntas:

  • ¿cómo se puede representar el conocimiento con la lógica de primer orden?,
  • ¿qué es una fórmula de primer orden?,
  • ¿qué significa que una fórmula verdadera? y
  • ¿qué significa que un argumento sea correcto?

Como ejemplos de representación hemos visto cómo representar conocimiento geográfico, del mundo de los bloques y conocimiento astronómico. En los distintos ejemplos hemos resaltado los tipos de símbolos lógicos utilizados.

A partir de los ejemplos de representación del conocimiento, se han definido los símbolos lógicos (variables, conectivas, cuantificadores e igualdad) y los símbolos no lógicos (constantes, predicados y funciones) que forman el alfabeto del lenguaje de la lógica de primer orden.

A partir del alfabeto, se definen los términos, las fórmulas atómicas y las fórmulas del lenguaje.

Como medio del reconocimiento de fórmulas, se introducen los árboles de análisis. Con ello, respondemos a la segunda de las preguntas iniciales.

En el estudio sintáctico, definimos el conjunto de las subfórmulas, el conjunto de las variables de un término, las ocurrencias libres y ligadas, el conjunto de las variables libres y ligadas y las fórmulas cerradas y abiertas. Algunas de las definiciones anteriores se realizan por recursión sobre fórmulas o sobre términos.

En segundo lugar hemos estudiado la semántica, comenzando con distintas cuestiones sobre qué significa que una fórmula sea verdadera para resaltar su dependencia del universo, la interpretación de los símbolos no lógico y de las asignaciones a las variables libres.

Se han definido las estructuras de un lenguaje, las asignaciones a las variables y las interpretaciones de un lenguaje.

Se ha definido el valor de un término o de una fórmula en una interpretación. Con ello, respondemos a la tercera de las preguntas iniciales.

Las transparencias de esta clase son las páginas 1 a 36 del tema 3.

Descargar (PDF, 310KB)

I1M2019: Cálculo simbólico con Maxima

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha continuado la presentación de Maxima como sistema de cálculo simbólico.

La presentación se ha realizado como una serie de relaciones de ejercicios resueltos. En concreto,

Finalmente se ha comentado la bibliografía disponible en la página de la asignatura:

Resumen de lecturas compartidas durante febrero de 2020

Esta entrada es una recopilación de lecturas compartidas, durante febrero de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante febrero de 2020”

Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms

Se ha publicado un artículo de razonamiento formalizado en Coq/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms.

Sus autores son

  • Christian Doczkal (Université Côte d’Azur, Inria Sopia Antipolis Méditerranée, France) y
  • Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).

Su resumen es

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

El trabajo se ha publicado en el Journal of Automated Reasoning

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