LI2011-12: 2º examen de la evaluación continua
En la clase de hoy del curso Lógica Informática se ha realizado el segundo examen de la evaluación continua.
Reseña: Formalization of propositional linear temporal logic in the Mizar system
Una línea de trabajo dentro del campo del razonamiento formalizado consiste en la formalización de la metalógica de distintos sistemas lógicos. En esta línea se inscribe el artículo Formalization of propositional linear temporal logic in the Mizar system.
Su autor es Mariusz Giero (University of Bialystok).
Su resumen es
The paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.
LI2011-12: Ejercicios de formas normales y resolución proposicional
En la clase de hoy del curso Lógica Informática se han comentados soluciones de ejercicios de formas normales y resolución proposicional. Los enunciados de los ejercicios se encuentran en los temas 3 y 4 del libro de ejercicios.
I1M2011: Patrones de definiciones por recursión en Haskell
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos visto los siguientes patrones de recursión:
- recursión sobre varios argumentos,
- recursión múltiple y
- recursión mutua.
Además, hemos visto una heurística para definir funciones por recursión.
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 6ª relación.
Las transparencias usadas en la clase son las comprendidas entre las páginas 13 y 30 del tema 6:
Read More “I1M2011: Patrones de definiciones por recursión en Haskell”
RA2011: Panorama del razonamiento automático mediante Otter, ACL2, PVS e Isabelle
En la clase de hoy del curso de Razonamiento automático se presentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.
Las transparencias de la clase son
Read More “RA2011: Panorama del razonamiento automático mediante Otter, ACL2, PVS e Isabelle”