{"batchcomplete":"","continue":{"lecontinue":"20210726120658|98","continue":"-||"},"query":{"logevents":[{"logid":108,"ns":0,"title":"Relaci\u00f3n 9","pageid":0,"logpage":74,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:10:23Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> chapter {* R9 Programaci\u00f3n funcional en Isabelle *}  theory R9 imports Main  begin  text {* ----------------------------------------------------------------   Ejercicio 0. Definir, por recursi\u00f3n, la fu\u2026\u00bb"},{"logid":107,"ns":0,"title":"Relaci\u00f3n 8","pageid":0,"logpage":67,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:09:56Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> chapter {* R8: Argumentaci\u00f3n en l\u00f3gica de primer orden *}  theory R8 imports Main  begin  text {*   ---------------------------------------------------------------------    El objetivo de esta relaci\u00f3\u2026\u00bb"},{"logid":106,"ns":0,"title":"Relaci\u00f3n 7","pageid":0,"logpage":65,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:09:34Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\">  theory R7 imports Main  begin  text {*   ---------------------------------------------------------------------    El objetivo de esta relaci\u00f3n es escribir demostraciones usando s\u00f3lo   las reglas b\u00e1si\u2026\u00bb"},{"logid":105,"ns":0,"title":"Relaci\u00f3n 5","pageid":0,"logpage":58,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:09:16Z","comment":"el contenido era: \u00ab=== Relaci\u00f3n 5: Sintaxis y sem\u00e1ntica de la L\u00f3gica de primer orden ===   ---- '''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de APPLI2), verificando la correcci\u00f3n de la soluci\u00f3n:  * Todo aquel que ent\u2026\u00bb"},{"logid":104,"ns":0,"title":"Relaci\u00f3n 4","pageid":0,"logpage":33,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:08:59Z","comment":"el contenido era: \u00ab<source lang=\"isabelle\"> chapter {* R4: Deducci\u00f3n natural proposicional *}  theory R4 imports Main  begin  text {*   ---------------------------------------------------------------------    El objetivo de esta relaci\u00f3n es demost\u2026\u00bb"},{"logid":103,"ns":0,"title":"Relaci\u00f3n 2","pageid":0,"logpage":17,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:08:27Z","comment":"el contenido era: \u00ab === Relaci\u00f3n 2: Deducci\u00f3n natural en l\u00f3gica proposicional ===   ---- '''Ejercicio 1.''' Demostrar mediante deducci\u00f3n natural: : p \u22a7 q \u2192 p ----  '''Soluci\u00f3n:'''  fravilval, roccorcor, sofsanfer, carespher, paurinara, anac\u2026\u00bb"},{"logid":102,"ns":0,"title":"Relaci\u00f3n 14","pageid":0,"logpage":86,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:08:06Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> theory R14 imports Main  begin  text {*   --------------------------------------------------------------------------------------------------   Ejercicio 1. Hilbert public\u00f3 una axiomatizaci\u00f3n de la geom\u2026\u00bb"},{"logid":101,"ns":0,"title":"Relaci\u00f3n 13","pageid":0,"logpage":84,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:07:50Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> chapter {* R13: Definiciones inductivas: clausuras *}  theory R13 imports Main begin  section {* La clausura reflexiva transitiva *}  text {*   \u00b7 Las definiciones inductivas aceptan par\u00e1metros; por tan\u2026\u00bb"},{"logid":100,"ns":0,"title":"Relaci\u00f3n 12","pageid":0,"logpage":82,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:07:31Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> chapter {* R12: Recorridos de \u00e1rboles *}  theory R12 imports Main  begin   text {*     ---------------------------------------------------------------------    Ejercicio 1. Definir el tipo de datos arbo\u2026\u00bb"},{"logid":99,"ns":0,"title":"Relaci\u00f3n 11","pageid":0,"logpage":78,"params":{},"type":"delete","action":"delete","user":"Jalonso","timestamp":"2021-07-26T12:07:15Z","comment":"el contenido era: \u00ab<source lang = \"isabelle\"> chapter {* R11: Razonamiento sobre programas en Isabelle/HOL *}   theory R11 imports Main  begin  text {* ---------------------------------------------------------------     En toda la relaci\u00f3n de ejerc\u2026\u00bb"}]}}