Source: https://www.glc.us.es/~jalonso/vestigium/tag/LI2013/
Timestamp: 2019-04-24 18:01:50+00:00

Document:
LI2013 | Vestigium
Etiqueta: LI2013
LI2013: Razonamiento en Prolog sobre listas
José A. Alonso- 10 enero 2014 -LI2013
En la clase de hoy del curso Lógica Informática se ha estudiado cómo se representan las listas en Prolog, cómo se diseñan programas sobre listas y cómo Prolog obtiene las respuestas.
Para la construcción de los árboles de deducción de Prolog se ha utilizado el programa SldDraw. El uso del programa se muestra en el siguiente vídeo.
La clase se basa en los apuntes de Introducción a la programación lógica con Prolog.
Las transparencias de esta clase son las página 18 a 27 del tema 12
LI2013-14: La lógica de Prolog
José A. Alonso- 8 enero 2014 -LI2013
En la clase de hoy del curso Lógica Informática se ha realizado una introducción a la programación lógica con Prolog como aplicación de la resolución en la lógica de primer orden.
Se ha presentado el sistema deductivo de Prolog en tres fases: proposicional, relacional y funcional. En cada una se ha comentado cómo representar el conocimiento, cómo realizar consultas y cómo es el razonamiento de Prolog para calcular las respuestas.
En los siguiente vídeos se presenta el uso de Prolog y uso de SldRaw.
Las transparencias de esta clase son las página 1 a 18 del tema 12
LI2013: Ejercicio de deducción en lógica de primer orden
José A. Alonso- 18 diciembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática se han comentado las soluciones de ejercicios de deducción en lógica de primer orden mediante los 3 métodos (deducción natural, tableros semánticos y resolució). Concretamente, los ejercicios comentados son desde el 5.1 al 5.9 del capítulo 8 del libro de ejercicios:
∀x [P(x) → Q(x)] ͱ ∀xP(x) → ∀xQ(x)
∃x ¬P(x) ͱ ¬∀xP(x)
∀xP(x) ͱ ∀yP(y)
∀x [P(x) → Q(x)] ͱ ∀x ¬Q(x) → ∀x ¬P(x)
∀x [P(x) → ¬Q(x)] ͱ ¬∃x [P(x) ∧ Q(x)]
∀x ∀yP(x,y) ͱ ∀u ∀vP(u,v)
∃x ∃yP(x,y) ͱ ∃u ∃vP(u,v)
∃x ∀yP(x,y) ͱ ∀y ∃xP(x,y)
∃x [P(a) → Q(x)] ͱ P(a) → ∃xQ(x)
LI2013: Ejercicios de resolución en lógica de primer orden
José A. Alonso- 13 diciembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática de han comentado las soluciones de ejercicios de resolución en lógica de primer orden. Concretamente, desde el ejercicio 13 al 14.5 del capítulo 12 del libro de ejercicios.
LI2013 Resolución en lógica de primer orden
José A. Alonso- 11 diciembre 2013 -LI2013
En la primera parte de la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.
En la segunda parte se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.
Las principales diferencias se encuentran en la unificación, separación de variables y factorización.
Como tarea pendientes se propone la resolución de los ejercicios de los temas 10 y 12 del libro de ejercicios.
Las transparencias de la primera parte son las del tema 10
LI2013: Tableros semánticos de primer orden y equivalencias lógicas
José A. Alonso- 4 diciembre 2013 -LI2013
En la primera parte de la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos de primer orden como ampliación del presentado en el tema 3 para la lógica proposicional.
En la segunda parte, se ha demostrado por deducción natural las principales equivalencias en lógica de primer orden. Además, se ha mostrado cómo hacer las demostraciones en Pandora como se muestra en este vídeo.
Las transparencias de esta clase son las finales del tema 8 y las del tema 9 que se muestran a continuación
LI2013: Deducción natural en lógica de primer orden (2)
José A. Alonso- 29 noviembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática se ha continuado el estudio de la deducción natural en lógica de primer orden. Se han comentado distintas equivalencias lógicas y se han demostrado por deducción natural y mediante tableros semánticos las siguientes equivalencias:
¬∀xP(x) ≡ ∃x¬P(x)
∀x(P(x) ∧ Q(x)) ≡ ∀xP(x) ∧ ∀xQ(x)
Las transparencias de esta clase son las páginas 14 a 20 del tema 8 que se muestran a continuación
LI2013: Deducción natural en lógica de primer orden
José A. Alonso- 27 noviembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática se presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores.
Las transparencias de esta clase son las páginas 1 a 13 del tema 8 que se muestran a continuación
LI2013: Semántica de la lógica de primer orden
José A. Alonso- 13 noviembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática se ha completado el estudio de la semántica de la lógica de primer orden introduciendo los conceptos de consistencia, consecuencia lógica y equivalencia. Se ha explicado la metodología de búqueda semántica de modelos y contramodelos.
Las transparencias de esta clase son las páginas 35 a 45 del tema 7:
LI2013: Ejercicios de resolución proposicional
José A. Alonso- 8 noviembre 2013 -LI2013
En la clase de hoy del curso Lógica Informática se han comentado soluciones de los ejercicios 21 a 25 del tema 5 del libro de ejercicios.
Problema de las puertas
Reparto de escaños por la ley d’Hont
Elementos no repetidos
Variación de la conjetura de Goldbach.
Matriz dodecafónica
I1M2018: El TAD de los multiconjuntos mediante diccionarios en Haskell
I1M2018: División y factorización de polinomios mediante la regla de Ruffini en Haskell
I1M2018: La librería de diccionarios en Haskell
LMF2018: Programación funcional con Isabelle/HOL
LMF2018: Primer examen de deducción natural con Isabelle/HOL
I1M2018: Ejercicios con el tipo abstracto de dato de los montículos
I1M2018: El TAD de los montículos en Haskell
Archivos Elegir mes abril 2019 (12) marzo 2019 (26) febrero 2019 (18) enero 2019 (12) diciembre 2018 (10) noviembre 2018 (16) octubre 2018 (19) septiembre 2018 (11) julio 2018 (4) junio 2018 (1) mayo 2018 (1) abril 2018 (13) marzo 2018 (25) febrero 2018 (21) enero 2018 (1) diciembre 2017 (12) noviembre 2017 (17) octubre 2017 (13) septiembre 2017 (7) julio 2017 (1) mayo 2017 (1) febrero 2017 (17) enero 2017 (3) diciembre 2016 (13) noviembre 2016 (19) octubre 2016 (14) septiembre 2016 (7) agosto 2016 (5) julio 2016 (5) mayo 2016 (12) abril 2016 (13) marzo 2016 (20) febrero 2016 (15) enero 2016 (10) diciembre 2015 (14) noviembre 2015 (16) octubre 2015 (20) septiembre 2015 (22) agosto 2015 (17) julio 2015 (3) junio 2015 (4) mayo 2015 (10) abril 2015 (14) marzo 2015 (15) febrero 2015 (17) enero 2015 (19) diciembre 2014 (25) noviembre 2014 (25) octubre 2014 (20) septiembre 2014 (15) julio 2014 (12) junio 2014 (5) mayo 2014 (10) abril 2014 (16) marzo 2014 (18) febrero 2014 (24) enero 2014 (25) diciembre 2013 (33) noviembre 2013 (26) octubre 2013 (29) septiembre 2013 (24) agosto 2013 (16) julio 2013 (12) junio 2013 (15) mayo 2013 (36) abril 2013 (45) marzo 2013 (23) febrero 2013 (18) enero 2013 (14) diciembre 2012 (21) noviembre 2012 (26) octubre 2012 (27) septiembre 2012 (13) agosto 2012 (19) julio 2012 (4) junio 2012 (4) mayo 2012 (5) abril 2012 (12) marzo 2012 (28) febrero 2012 (20) enero 2012 (14) diciembre 2011 (20) noviembre 2011 (29) octubre 2011 (17) septiembre 2011 (10) agosto 2011 (11) julio 2011 (10) junio 2011 (7) mayo 2011 (15) abril 2011 (16) marzo 2011 (19) febrero 2011 (22) enero 2011 (14) diciembre 2010 (19) noviembre 2010 (26) octubre 2010 (18) septiembre 2010 (22) agosto 2010 (25) julio 2010 (2) marzo 2010 (3) febrero 2010 (16) enero 2010 (26)

References: resolución 
 resolución 
 resolución 
 Resolución 
 resolución 
 resolución 
 resolución