Diferencia entre revisiones de «Temas»
De Demostración automática de teoremas (2014-15)
| Línea 3: | Línea 3: | ||
*[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.] | ||
* Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL. | * Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL. | ||
| − | *[http://www.cs.us.es/~mjoseh/dat-15/tema- | + | *[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- | + | *[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. | * Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL. | ||
* Tema 7: Programación funcional en Isabelle/HOL. | * Tema 7: Programación funcional en Isabelle/HOL. | ||
Revisión del 12:50 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.
- Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL.
- Tema 7: Programación funcional en Isabelle/HOL.
- Tema 8: Razonamiento sobre programas en Isabelle/HOL.
- Tema 9: Razonamiento estructurado en Isabelle/HOL.
- Tema 10: Razonamiento por casos e inducción.
- Tema 11: Verificación de algoritmos deordenación.
- Tema 12: Conjuntos, funciones y relaciones.
- Tema 13: Definiciones inductivas en Isabelle/HOL
- Tema 14: Caso de estudio: clausura reflexiva transitiva.
- Tema 15: Razonamiento modular: Teoría de grupos.