https://www.glc.us.es/web/index.php?action=history&feed=atom&title=Seminarios_anterioresSeminarios anteriores - Historial de revisiones2026-07-17T14:57:18ZHistorial de revisiones para esta página en el wikiMediaWiki 1.31.0https://www.glc.us.es/web/index.php?title=Seminarios_anteriores&diff=134&oldid=prevJalonso: New page: == Seminarios del curso 2007-08 == === Seminario del 9 de Julio de 2008 === * '''Título:''' ''El papel de ACL2 para incrementar la fiabilidad de Kenzo'' * '''Ponente:''' *: [https://bel...2008-10-08T10:22:46Z<p>New page: == Seminarios del curso 2007-08 == === Seminario del 9 de Julio de 2008 === * '''Título:''' ''El papel de ACL2 para incrementar la fiabilidad de Kenzo'' * '''Ponente:''' *: [https://bel...</p>
<p><b>Página nueva</b></p><div>== Seminarios del curso 2007-08 ==<br />
<br />
=== Seminario del 9 de Julio de 2008 ===<br />
* '''Título:''' ''El papel de ACL2 para incrementar la fiabilidad de Kenzo''<br />
* '''Ponente:''' <br />
*: [https://belenus.unirioja.es/~mirandre/ Mirian Andrés]<br />
*: [http://www.unirioja.es/dptos/dmc/index.shtml Departamento de Matemáticas y Computación]<br />
*: [http://www.unirioja.es/ Universidad de La Rioja]<br />
* '''Resumen:''' La charla consiste en presentar de forma divulgativa una de las lineas de investigación de un grupo de la Universidad de La Rioja. Se explicarán los intereses en el uso de ACL2 y, de forma un poco más formal se mostrará, a modo de ejemplo, el trabajo [http://www.cs.uwyo.edu/~ruben/acl2-07/uploads/Main/007.pdf Formalizing Simplicial Topology in ACL2] presentado en el pasado [http://www.cs.uwyo.edu/~ruben/acl2-07/Main/HomePage Workshop de ACL2 de 2007].<br />
----<br />
<br />
=== Seminario del 30 de Junio de 2008 ===<br />
* '''Título:''' ''Razonamiento conjuntista en Isabelle/Isar''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se presenta cómo puede razonarse con conjuntos definidos por comprensión y conjuntos finitos en Isabelle/Isar. El contenido del seminario se corresponde con el capítulo 7 de {{IDAO}}.<br />
----<br />
<br />
=== Seminario del 23 de Junio de 2008 ===<br />
* '''Título:''' ''Métodos formales: pasado, presente y futuro''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se comenta el estado actual de los métodos formales a partir de de las comunicaciones presentadas en [http://qpq.csl.sri.com/files Formal Methods Outreach Workshop] (SRI Junio de 2008). <br />
----<br />
<br />
=== Seminario del 16 de Junio de 2008 ===<br />
* '''Título:''' ''Sensor-IA''<br />
* '''Ponente:''' {{fmartin}}<br />
* '''Resumen:''' Se realizará una presentación del proyecto "Sensor-IA" realizado para el Instituto Andaluz de Tecnología.<br />
----<br />
<br />
=== Seminario del 9 de Junio de 2008 ===<br />
* '''Título:''' ''Demostración en Isar de la corrección de un compilador''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se presenta, como caso de estudio en Isar, la demostración de la corrección de un compilador. El contenido del seminario se corresponde con el capítulo 6 de {{IDAO}}.<br />
----<br />
<br />
=== Seminario del 26 de Mayo de 2008 ===<br />
* '''Título:''' ''Patrones de razonamiento en Isabelle/Isar''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se extienden los patrones de razonamiento proposicional, cuantificacional e inductivo de Isabelle/Isar. Se pondrá el énfasis en las demostraciones estructuradas. El contenido del seminario se corresponde con los capítulos 4 y 5 de {{IDAO}}.<br />
----<br />
<br />
=== Seminario del 19 de Mayo de 2008 === <br />
* '''Título:''' ''APLI2: pasado, presente y futuro.''<br />
* '''Ponente:''' {{garanda}}<br />
* '''Resumen:''' [http://www.glc.us.es/apli2 APLI2] es un sistema desarollado para la ayuda a la enseñanza de la Lógica. En esta charla describiremos tanto la arquitectura del sistema como usabilidad y posibles ampliaciones del sistema.<br />
----<br />
<br />
=== Seminario del 12 de Mayo de 2008 ===<br />
* '''Título:''' ''Razonamiento inductivo en Isabelle/Isar''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se presentan los patrones de razonamiento por inducción matemática y por inducción estructural en Isabelle/Isar. El contenido del seminario se corresponde con el capítulo 3 de {{IDAO}}.<br />
----<br />
<br />
=== Seminario del 5 de Mayo de 2008 ===<br />
* '''Título:''' ''Patrones básicos de razonamiento en Isabelle/Isar''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' En este seminario se presentan los patrones básicos de Isabelle/Isar para el razonamiento proposicional, cuantificacional y ecuacional. Se pondrá el énfasis en las demostraciones estructuradas. El contenido del seminario se corresponde con el capítulos 2 de {{IDAO}}.<br />
----<br />
<br />
=== Seminario del 28 de Abril de 2008 === <br />
* '''Título:''' ''Isabelle como lenguaje de programación e Isar como lenguaje de demostración''<br />
* '''Ponente:''' {{jalonso}}<br />
* '''Resumen:''' Este seminario es el primero de una serie cuyo objetivo es mostrar las posibilidades de Isabelle/Isar como sistema que permite regular el nivel de automatización de las demostraciones y hacerlas legibles por los humanos y procesable por las máquinas. El contenido del seminario se corresponde con los dos primeros capítulos de {{IDAO}}.<br />
----</div>Jalonso