Diferencia entre revisiones de «Temas»
De DAO (Demostración asistida por ordenador)
(→Temas de Demostración asistida por ordenador) |
(→Temas de Demostración asistida por ordenador) |
||
| Línea 2: | Línea 2: | ||
* [[Tema 7: Programación funcional en Isabelle]]. | * [[Tema 7: Programación funcional en Isabelle]]. | ||
* [[Tema 8: Razonamiento sobre programas]]. | * [[Tema 8: Razonamiento sobre programas]]. | ||
| − | * [[Tema | + | * [[Tema 1: Deducción natural proposicional con Isabelle/HOL]]. |
* [[Tema 4: Deducción natural en lógica de primer orden en Isabelle/HOL]]. | * [[Tema 4: Deducción natural en lógica de primer orden en Isabelle/HOL]]. | ||
* [[Tema 5: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica]]. | * [[Tema 5: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica]]. | ||
* [[Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL]]. | * [[Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL]]. | ||
Revisión del 08:31 14 mar 2013
Temas de Demostración asistida por ordenador
- Tema 7: Programación funcional en Isabelle.
- Tema 8: Razonamiento sobre programas.
- Tema 1: Deducción natural proposicional con Isabelle/HOL.
- Tema 4: Deducción natural en lógica de primer orden en Isabelle/HOL.
- Tema 5: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica.
- Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL.