En la clase de hoy del curso de Demostración asistida por ordenador se se ha estudiado cómo escribir demostraciones mediante deducción natural en lógica de primer orden usando Isabelle/HOL/Isar.
La teoría correspondiente a la clase es Tema_3.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Deducción natural en lógica de primer orden con Isabelle/HOL”
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado la introducción al estudio de grafos.
En primer lugar, hemos visto cómo se puede generar familas de grafos como los grafos completos de orden n y los ciclos de orden n, que se usarán en la relación 30 de ejercicios. Estos y otros ejemplos se pueden ver en la galería de grafos de Wikipedia.
A continuación, se ha explicado cómo pueden construirse y representarse estos grafos con Maxima. Las instrucciones se encuentran en el capítulo 57 del manual de Maxima.