Diferencia entre revisiones de «Temas»
De Demostración automática de teoremas (2014-15)
Línea 2: | Línea 2: | ||
*[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-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.] | *[http://www.cs.us.es/~mjoseh/dat-15/tema-2.pdf Tema 2: Deducción natural en Lógica proposicional.] | ||
− | *[http://www.cs.us.es/~mjoseh/dat-15/tema-3.pdf Tema | + | * Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL. |
− | *[http://www.cs.us.es/~mjoseh/dat-15/tema-4.pdf Tema | + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-3.pdf Tema 4: Sintaxis y semántica de la Lógica de primer orden.] |
− | + | *[http://www.cs.us.es/~mjoseh/dat-15/tema-4.pdf Tema 5: Deducción natural en Lógica de primer orden.] | |
− | * T6: Deducción natural en Lógica de primer orden con Isabelle/ | + | * T6: Deducción natural en Lógica de primer orden con Isabelle/HOL. |
− | + | * T7: Programación funcional en Isabelle/HOL. | |
− | * T7: Programación funcional en Isabelle/ | + | * T8: Razonamiento sobre programas en Isabelle/HOL. |
− | * T8: Razonamiento sobre programas en Isabelle/ | ||
* T9: Razonamiento estructurado en Isabelle/HOL. | * T9: Razonamiento estructurado en Isabelle/HOL. | ||
* T10: Razonamiento por casos e inducción. | * T10: Razonamiento por casos e inducción. | ||
Línea 15: | Línea 14: | ||
* T13: Definiciones inductivas en Isabelle/HOL | * T13: Definiciones inductivas en Isabelle/HOL | ||
* T14: Caso de estudio: clausura reflexiva transitiva. | * T14: Caso de estudio: clausura reflexiva transitiva. | ||
− | |||
* T15: Razonamiento modular: teoría de grupos. | * T15: Razonamiento modular: teoría de grupos. |
Revisión del 10:31 20 feb 2015
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.
- Tema 4: Sintaxis y semántica de la Lógica de primer orden.
- Tema 5: Deducción natural en Lógica de primer orden.
- T6: Deducción natural en Lógica de primer orden con Isabelle/HOL.
- T7: Programación funcional en Isabelle/HOL.
- T8: Razonamiento sobre programas en Isabelle/HOL.
- T9: Razonamiento estructurado en Isabelle/HOL.
- T10: Razonamiento por casos e inducción.
- T11: Verificación de algoritmos deordenación.
- T12: Conjuntos, funciones y relaciones.
- T13: Definiciones inductivas en Isabelle/HOL
- T14: Caso de estudio: clausura reflexiva transitiva.
- T15: Razonamiento modular: teoría de grupos.