Páginas nuevas
- 14:08 14 feb 2019 Tema 7: Definiciones inductivas en Coq (hist) [18 128 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> (* T7: Proposiciones definidas inductivamente *) Set Warnings "-notation-overridden,-parsing". Require Export T6_Logica. Require Coq.omega.Omega. (* E…»)
- 13:46 14 feb 2019 Tema 6: Lógica en Coq (hist) [80 060 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> Set Warnings "-notation-overridden,-parsing". Require Export T5_Tacticas. (* El contenido del tema es 1. Introducción 2. Conectivas lógicas…»)
- 08:34 14 feb 2019 Tema 5: Tácticas básicas de Coq (hist) [52 599 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> Set Warnings "-notation-overridden,-parsing". Require Export T4_PolimorfismoyOS. Require Export R2_Induccion_sol. (* El contenido del tema es 1. La…»)
- 08:33 14 feb 2019 Tema 4: Polimorfismo y funciones de orden superior en Coq (hist) [22 702 bytes] Jalonso (discusión | contribuciones) (Página creada con «Require Export T3_EstructurasNat. (* El contenido del tema es 1. Polimorfismo 1. Listas polimórficas 1. Inferencia de tipos 2. Síntesis de l…»)
- 08:31 14 feb 2019 Tema 3: Datos estructurados en Coq (hist) [28 608 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> Require Export T2_Induccion. (* En este capítulos se estudian datos estructurados con números naturales. Su contenido es 1. Pares de números…»)
- 08:30 14 feb 2019 Tema 2: Demostraciones por inducción sobre los números naturales en Coq (hist) [4617 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> Require Export T1_PF_en_Coq. (* El contenido de la teoría es 1. Demostraciones por inducción. 2. Demostraciones anidadas. 3. Demostraciones…»)
- 08:30 14 feb 2019 Tema 1: Programación funcional y métodos elementales de demostración en Coq (hist) [26 086 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="coq"> (* El contenido de la teoría es 1. Datos y funciones 1. Tipos enumerados 2. Booleanos 3. Tipos de las funciones 4. Tipos compuestos…»)
- 09:02 9 feb 2019 Relación 8 (hist) [26 545 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R8: Gramáticas libres de contexto *} theory R8_Gramaticas_libre_de_contexto imports Main begin text {* En esta relación se definen…»)
- 09:02 9 feb 2019 R8 (hist) [3945 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R8: Gramáticas libres de contexto *} theory R8_Gramaticas_libre_de_contexto imports Main begin text {* En esta relación se definen…»)
- 14:08 7 feb 2019 Tema 12: Conjuntos, funciones y relaciones (hist) [15 598 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* Tema 12: Conjuntos, funciones y relaciones *} theory T12_Conjuntos_funciones_y_relaciones imports Main begin section {* Conjuntos *}…»)
- 14:06 7 feb 2019 Tema 11: Definiciones inductivas (hist) [6880 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* Tema 11: Definiciones inductivas *} theory T11_Definiciones_inductivas imports Main begin section {* El conjunto de los números pares…»)
- 17:53 30 ene 2019 Tema 10: Caso de estudio: Compilación de expresiones (hist) [8576 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* Tema 10: Caso de estudio: Compilación de expresiones *} theory T10_Caso_de_estudio_Compilacion_de_expresiones imports Main begin dec…»)
- 11:18 24 ene 2019 Tema 9: Editores lógicos (hist) [1279 bytes] Jalonso (discusión | contribuciones) (Página creada con «== Deducción natural con Pandora == * El sitio de Pandora es [http://www.doc.ic.ac.uk/pandora/newpandora] (o su [https://www.cs.us.es/~jalonso/cursos/lmf/sistemas/pandor…»)
- 10:40 24 ene 2019 Relación 7 (hist) [28 792 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R7: Deducción natural de primer orden *} theory R7_Deduccion_natural_de_primer_orden imports Main begin text {* Demostrar o refuta…»)
- 10:40 24 ene 2019 R7 (hist) [6868 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R7: Deducción natural de primer orden *} theory R7_Deduccion_natural_de_primer_orden imports Main begin text {* Demostrar o refuta…»)
- 10:30 24 ene 2019 Tema 8b: Deducción natural en lógica de primer orden con Isabelle/HOL (hist) [16 659 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle" chapter {* Tema 8b: Deducción natural en lógica de primer orden *} theory T8b_Deduccion_natural_en_logica_de_primer_orden imports Main begin te…»)
- 20:08 9 ene 2019 Colaboraciones (hist) [539 bytes] Jalonso (discusión | contribuciones) (Página creada con «=== Colaboraciones en todas la relaciones === <source lang="text"> | 69 | pabalagon | | 69 | cammonagu | | 64 | benber | | 64 | alfmarcua | | 63 | josgomro…»)
- 19:39 9 ene 2019 Relación 6 (hist) [57 589 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R6: Deducción natural proposicional *} theory R6_Deduccion_natural_proposicional imports Main begin text {* ----------------------…»)
- 19:39 9 ene 2019 R6 (hist) [17 747 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R6: Deducción natural proposicional *} theory R6_Deduccion_natural_proposicional imports Main begin text {* ----------------------…»)
- 19:24 9 ene 2019 Tema 7b: Deducción natural proposicional con Isabelle/HOL (hist) [25 608 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* Tema 7b: Deducción natural proposicional con Isabelle/HOL *} theory T7b_Deduccion_natural_en_logica_proposicional_con_Isabelle imports…»)
- 07:59 14 dic 2018 Relación 5 (hist) [20 678 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R5: Recorridos de árboles *} theory R5_Recorridos_de_arboles imports Main begin text {* ---------------------------------------…»)
- 07:59 14 dic 2018 R5 (hist) [7077 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* R5: Recorridos de árboles *} theory R5_Recorridos_de_arboles imports Main begin text {* ---------------------------------------…»)
- 14:35 13 dic 2018 Tema 6b: Verificación de la ordenación por mezcla (hist) [7292 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* T6b: Verificación de la ordenación por mezcla *} theory T6b_Verificacion_de_la_ordenacion_por_mezcla imports Main begin text {* En…»)
- 14:28 13 dic 2018 Tema 6a: Verificación de la ordenación por inserción (hist) [10 712 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* T6a: Verificación de la ordenación por inserción *} theory T6a_Verificacion_de_la_ordenacion_por_insercion imports Main begin text…»)
- 14:21 13 dic 2018 Tema 5: Razonamiento sobre árboles y bosques (hist) [8470 bytes] Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* Tema 5: Razonamiento sobre árboles *} theory T5_Razonamiento_sobre_arboles imports Main HOL.Parity begin text {* En este tema se es…»)