Diferencia entre revisiones de «Temas»
De Demostración automática de teoremas (2014-15)
(Página creada con '== Temas de ''Demostración automática de teoremas (2014-15)'' ==') |
|||
| (No se muestran 27 ediciones intermedias de 2 usuarios) | |||
| Línea 1: | Línea 1: | ||
== Temas de ''Demostración automática de teoremas (2014-15)'' == | == Temas de ''Demostración automática de teoremas (2014-15)'' == | ||
| + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-1.pdf Tema 1: Sintaxis y semántica de la Lógica proposicional.] | ||
| + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-2.pdf Tema 2: Deducción natural en Lógica proposicional.] | ||
| + | * [[Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL]].[http://www.cs.us.es/~mjoseh/dat-15/T3.thy] | ||
| + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-4.pdf Tema 4: Sintaxis y semántica de la Lógica de primer orden.] | ||
| + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-5.pdf Tema 5: Deducción natural en Lógica de primer orden.] | ||
| + | * [[Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL]].[http://www.cs.us.es/~mjoseh/dat-15/T6.thy] | ||
| + | * [[Tema 7: Programación funcional en Isabelle/HOL.]][http://www.cs.us.es/~mjoseh/dat-15/T7.thy] | ||
| + | * [[Tema 8: Razonamiento sobre programas en Isabelle/HOL.]][http://www.cs.us.es/~mjoseh/dat-15/T8.thy] | ||
| + | * [[Tema 9: Razonamiento por casos e inducción.]][http://www.cs.us.es/~mjoseh/dat-15/T9.thy] | ||
| + | * [[Tema 10: Conjuntos, funciones y relaciones.]][http://www.cs.us.es/~mjoseh/dat-15/T10.thy] | ||
| + | * [[Tema 11: Métodos de demostración.]][http://www.cs.us.es/~mjoseh/dat-15/T11.thy] | ||
| + | * [[Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.]][http://www.cs.us.es/~mjoseh/dat-15/T12.thy] | ||
| + | * [[Tema 13: Razonamiento modular (I): Teoría de grupos.]][http://www.cs.us.es/~mjoseh/dat-15/T13.thy] | ||
| + | * [[Tema 14: Razonamiento modular (II): Órdenes y retículos.]][http://www.cs.us.es/~mjoseh/dat-15/T14.thy] | ||
| + | * Razonamiento modular (III): Interpretaciones de teorías: | ||
| + | ** [[Tema 15(a): sustitución de parámetros.]][http://www.cs.us.es/~mjoseh/dat-15/T15a.thy] | ||
| + | ** [[Tema 15(b): sustitución de definiciones.]][http://www.cs.us.es/~mjoseh/dat-15/T15b.thy] | ||
| + | ** [[Tema 15(c): interpretaciones locales.]][http://www.cs.us.es/~mjoseh/dat-15/T15c.thy] | ||
Revisión actual del 14:49 25 feb 2016
Temas de Demostración automática de teoremas (2014-15)
- Tema 1: Sintaxis y semántica de la Lógica proposicional.
- Tema 2: Deducción natural en Lógica proposicional.
- Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL.[1]
- Tema 4: Sintaxis y semántica de la Lógica de primer orden.
- Tema 5: Deducción natural en Lógica de primer orden.
- Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL.[2]
- Tema 7: Programación funcional en Isabelle/HOL.[3]
- Tema 8: Razonamiento sobre programas en Isabelle/HOL.[4]
- Tema 9: Razonamiento por casos e inducción.[5]
- Tema 10: Conjuntos, funciones y relaciones.[6]
- Tema 11: Métodos de demostración.[7]
- Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.[8]
- Tema 13: Razonamiento modular (I): Teoría de grupos.[9]
- Tema 14: Razonamiento modular (II): Órdenes y retículos.[10]
- Razonamiento modular (III): Interpretaciones de teorías: