Diferencia entre revisiones de «Seminario del Grupo de Lógica Computacional»

De WikiGLC
Saltar a: navegación, buscar
(→‎Seminario del 18 de Junio de 2010)
 
(No se muestran 151 ediciones intermedias de 5 usuarios)
Línea 1: Línea 1:
−
Los Seminarios del Grupo de Lógica Computacional se celebrarán, salvo excepciones, los miércoles de 12:30 a 13:30 en el seminario del módulo L4 del Departamento de Ciencias de la Computación e Inteligencia Artificial. Las sesiones son abiertas y pueden acudir todas las personas interesadas.
+
__NOTOC__
 +
Los Seminarios del Grupo de Lógica Computacional se celebrarán en el seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial. Las sesiones son abiertas y pueden acudir todas las personas interesadas.
  
−
[[image:Sello-us.jpg]]  
+
== Próximas sesiones del seminario ==
−
* '''UNIVERSIDAD DE SEVILLA. VICERRECTORADO DE RELACIONES INSTITUCIONALES'''
+
 
−
** '''Las actividades de este seminario han sido financiadas parcialmente con una ayuda de Extensión universitaria de la Universidad de Sevilla
+
=== <span id="5-abril-17">Seminario del 5 de abril de 2017</span> ===
−
'''
+
* '''Título:''' ''Diseño de una plataforma para simulación de dispositivos inalámbricos''
 +
* '''Ponente:''' {{garanda}} (Grupo de Lógica Computacional - Universidad de Huelva).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:30 a 12:30.
 +
* '''Resumen:''' Aplicación de la tecnología multiagente JADE para la construcción de una plataforma de simulación de dispositivos inalámbricos.
 +
 
 +
== Sesiones anteriores del seminario ==
 +
 
 +
=== <span id="30-Marzo-16">Seminario del 30 de marzo de 2016</span> ===
 +
* '''Título:''' ''Introducción a ROS con Deep Learning Robot''
 +
* '''Ponente:''' [http://diegocabrera.info Diego R. Cabrera Mendieta] (Universidad Politécnica Salesiana, Ecuador).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:15 a 12:15.
 +
* '''Resumen:''' Las aplicaciones de la Inteligencia Artificial a la robótica están revolucionando el mundo actual. El comportamiento de los robots cada vez presenta más características "inteligentes". En este seminario vamos a ver distintas aplicaciones de inteligencia artificial ejecutadas sobre la plataforma [https://www.autonomous.ai/deep-learning-robot Deep Learning Robot] y programadas usando como framework base el [https://en.wikipedia.org/wiki/Robot_Operating_System sistema operativo para robots (ROS)].
 +
 
 +
=== <span id="10-Febrero-16">Seminario del 10 de febrero de 2016</span> ===
 +
* '''Título:''' ''Buscando un modelo: lógicas modales, semántica y decibilidad''
 +
* '''Ponente:''' [http://liis.famaf.unc.edu.ar/people/guillaume-hoffmann-0 Guillaume Hoffmann] (Universidad Nacional de Córdoba, Argentina).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:15 a 12:15.
 +
* '''Resumen:''' En términos de expresividad y de comportamiento computacional, la lógicas modales están ubicadas entre la lógica proposicional y la lógica del primer orden. En esta charla vamos a ver porqué, y técnicas para demostrar la decibilidad o indecibilidad de una lógica: métodos de tableros y reducciones.
 +
 
 +
=== <span id="17-Diciembre-15">Seminario del 17 de diciembre de 2015</span> ===
 +
* '''Título:''' ''Darcs: control de versiones para principiantes''
 +
* '''Ponente:''' [http://liis.famaf.unc.edu.ar/people/guillaume-hoffmann-0 Guillaume Hoffmann] (Universidad Nacional de Córdoba, Argentina).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 16:30 a 18:30.
 +
* '''Resumen:''' En el área del desarrollo de software, el control de versiones permite agilizar muchas tareas rutinarias. Involucra un software que ayuda al programador a guardar las distintas versiones de un software en desarrollo, y hacer ciertas operaciones sobres esas. <p>En esta charla presentaré el software [http://darcs.net Darcs]. Darcs es un sistema de control de versiones distribuido, libre y escrito en Haskell. Darcs es amigable: tiene un modelo de funcionamento accesible para usuarios inexpertos. Compararé Darcs con otros SCV (Git y Subversion) y presentaré unas ideas de proyectos que pueden interesar a estudiantes de informática.</p> <p> Ver también: [http://tinyurl.com/darcsensevilla Darcs en Sevilla].</p>
 +
 
 +
=== <span id="16-Diciembre-15">Seminario del 16 de diciembre de 2015</span> ===
 +
* '''Título:''' ''Darcs: un sistema de control de versiones distribuido''
 +
* '''Ponente:''' [http://liis.famaf.unc.edu.ar/people/guillaume-hoffmann-0 Guillaume Hoffmann] (Universidad Nacional de Córdoba, Argentina).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:15 a 12:15.
 +
* '''Resumen:''' [https://es.wikipedia.org/wiki/Darcs Darcs] es un sistema de control de versiones distribuido con un énfasis en la verificación de la corrección (utilizando Haskell y QuickCheck). En el seminario se explicará el uso y fundamento de Darcs.<br>Más información en [https://dl.dropboxusercontent.com/u/6239815/sevilla/index.html Darcs en Sevilla].
 +
 
 +
=== <span id="19-Junio-15">Seminario del 19 de junio de 2015</span> ===
 +
* '''Título:''' ''Structure and Real-world SAT Solving''
 +
* '''Ponente:''' [http://www.iiia.csic.es/~jgiraldez/home Jesús Giráldez Crú] (Artificial Intelligence Research Institute IIIA-CSIC, Barcelona).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:30 a 12:30.
 +
* '''Resumen:''' The Boolean Satisfiability problem (SAT) is the first known NP-complete problem. Besides its complexity, it is extensively used to solve practical applications (such as planning, scheduling or formal verification, among others). Modern SAT solvers have experienced a remarkable progress on solving these industrial (or real-world) SAT instances. Most of the techniques have been developed after an intensive experimental testing process. The common wisdom in the SAT community is that the success of these techniques is because they exploit some kind of hidden structure that industrial formulas actually have. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them. <br>In this talk, we analyze some structural properties of SAT instances, viewed as graphs. Namely, they are the scale-free structure, the community structure and the self-similar structure. In addition, we explore how these graph properties are affected during SAT solving by effects of variable instantiation or clause learning. Finally, we present some applications in SAT solving based on these notions of structure.
 +
 
 +
=== <span id="29-Abril-15">Seminario del 29 de abril de 2015</span> ===
 +
* '''Título:''' ''Enumeración de los racionales''
 +
* '''Ponente:''' David Argullo
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen:''' El código comentado correspondiente a la charla se encuentra en [http://bit.ly/1Aphv2k esta página].
 +
 
 +
=== <span id="15-Abril-15">Seminario del 15 de abril de 2015</span> ===
 +
* '''Título:''' ''Los teoremas de incompletitud de Gödel''
 +
* '''Ponente:''' Xavier Seguí
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen: '''El objetivo del seminario es presentar los dos teoremas de incompletitud de Kurt Gödel, dando una visión conceptual de ellos. Dado que son dos de los resultados más profundos y paradójicos de la lógica matemática, se verá alguna aplicación tanto dentro como fuera del ámbito matemático.
 +
 
 +
=== <span id="11-Marzo-15">Seminario del 11 de marzo de 2015</span> ===
 +
* '''Título:''' ''El algoritmo de Huffmann en Isabelle/HOL''
 +
* '''Ponente:''' David Rasero
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen:''' El algoritmo de Huffman es un algoritmo para la codificación de datos, desarrollado por David A. Huffman en 1952. El objetivo del seminario es describir el algoritmo y esbozar una prueba formal de la corrección de este algoritmo, usando Isabelle/HOL.
 +
 
 +
=== <span id="18-Marzo-15">Seminario del 18 de marzo de 2015</span> ===
 +
* '''Título:''' ''El algoritmo de unificación.''
 +
* '''Ponente:''' María Barranca
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen:''' El objetivo del seminario es describir el algoritmo de unificación y esbozar una formalización del mismo en Isabelle/HOL.
 +
 
 +
=== <span id="4-Marzo-15">Seminario del 4 de marzo de 2015</span> ===
 +
* '''Título:''' ''Un algoritmo en tiempo lineal para construir un árbol de altura mínima (2ª parte)''
 +
* '''Ponente:''' Daniel Rodríguez
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen:''' Consideramos el problema de construir un árbol de altura mínima, cuya frontera sea una lista dada. Se analizan dos algoritmos, uno de ellos recursivo (o top-down) y el otro iterativo (o bottom-up). Aunque se    obtienen árboles diferentes, ambos pueden implementarse en tiempo lineal en Haskell.
 +
 
 +
=== <span id="25-Febrero-15">Seminario del 25 de febrero de 2015</span> ===
 +
* '''Título:''' ''Un algoritmo en tiempo lineal para construir un árbol de altura mínima''
 +
* '''Ponente:''' Daniel Rodríguez
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:45 a 11:30.
 +
* '''Resumen:''' Consideramos el problema de construir un árbol de altura mínima, cuya frontera sea una lista dada. Se analizan dos algoritmos, uno de ellos recursivo (o top-down) y el otro iterativo (o bottom-up). Aunque se    obtienen árboles diferentes, ambos pueden implementarse en tiempo lineal en Haskell.
 +
 
 +
=== <span id="18-Febrero-15">Seminario del 18 de febrero de 2015</span> ===
 +
* '''Título:''' ''Algoritmo en tiempo lineal para buscar el menor objeto no usado''
 +
* '''Ponente:''' Javier Rodríguez
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Un problema frecuente en programación es, dado un conjunto de objetos en uso, encontrar el menor objeto que no se está usando, entre todos los objetos susceptibles de ser usados. En esta sesión se describirán dos soluciones al problema en tiempo lineal y sus implementaciones en Haskell.
 +
 
 +
=== <span id="11-Febrero-15">Seminario del 11 de febrero de 2015</span> ===
 +
* '''Título:''' ''Perlas de programación funcional''
 +
* '''Ponente:''' María José Hidalgo
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Hoy se inicia una serie de sesiones dedicadas a la exposición de "Perlas de programación funcional", basadas en:
 +
** [https://books.google.es/books?id=ZQJnYoAmw6gC&printsec=frontcover#v=onepage&q&f=false Pearls of Functional Algorithm Design]
 +
** [https://wiki.haskell.org/Research_papers/Functional_pearls Functional Pearls]
 +
 
 +
=== <span id="3-Marzo-14">Seminario del 3 de marzo de 2014</span> ===
 +
* '''Título:''' ''Presentación de Terms''
 +
* '''Ponente:''' Enrique Pérez Arnaud
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 17:00 a 18:00.
 +
* '''Resumen:''' Terms es un sistema basado en reglas, capaz de mantener bases de conocimiento persistentes, y de extraer deducciones de las mismas. El lenguaje en el que se expresa el conocimiento (reglas y hechos) es original del sistema, está basado en una teoría de primer orden, y está diseñado para expresar con sencillez el mismo tipo de conocimiento que se expresa normalmente con el lenguaje natural.
 +
 
 +
=== <span id="15-Enero-14">Seminario del 29 de enero de 2014</span> ===
 +
* '''Título:''' ''Laboratorio de Sistemas Multiagente con JADE''
 +
* '''Ponente:''' Gonzalo A. Aranda Corral
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:30 a 12:30.
 +
* '''Resumen:''' En esta sesión se realizará una introducción práctica a la plataforma JADE para sistemas multiagente
 +
 
 +
=== <span id="27-Noviembre-13">Seminario del 27 de noviembre de 2013</span> ===
 +
* '''Título:''' ''Formalización de la prueba de la trascendencia del número e''
 +
* '''Ponente:''' Pedro G. Ros Reina
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:30 a 13:30.
 +
* '''Resumen:''' En la charla se explicará la prueba de Hermite de que el número e es trascendente y la [http://jfr.unibo.it/article/view/2269/1749 formalización de Jesse Bingham] en [http://www.cl.cam.ac.uk/~jrh13/hol-light/ HOL Light].
 +
 
 +
=== <span id="16-Octubre-13">Seminario del 16 de octubre de 2013</span> ===
 +
* '''Título:''' ''Desarrollo colaborativo de programas: Git''
 +
* '''Ponente:''' Pedro Almagro Blanco
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:30 a 13:30.
 +
* '''Resumen:''' Introducción al desarrollo de software de forma colaborativa usando como soporte la [http://git-scm.com/ plataforma Git].
 +
 
 +
=== <span id="16-Mayo-13">Seminario del 16 de mayo de 2013</span> ===
 +
* '''Título:''' ''Formalización de la Relatividad (especial) en lógica de primer orden. Parte II''
 +
* '''Ponente:''' {{garanda}} (Grupo de Lógica Computacional - Universidad de Huelva)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:00 a 13:00.
 +
* '''Resumen:''' En esta charla se continuará con la formalización de la RE, terminando con la demostración de un teorema.
 +
 
 +
=== <span id="11-Abril-13">Seminario del 11 de abril de 2013</span> ===
 +
* '''Título:''' ''Formalización de la Relatividad (especial) en lógica de primer orden. Introducción''
 +
* '''Ponente:''' {{garanda}} (Grupo de Lógica Computacional - Universidad de Huelva)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' En esta charla se comenzará la formalización de la Relatividad Especial(RE), estableciendo las bases de la representación del conocimiento y traduciendo los axiomas de la RE en enunciados lógicos.
 +
 
 +
=== <span id="16-Enero-13">Seminario del 16 de enero de 2013</span> ===
 +
* '''Título:''' ''Relatividad (especial)''
 +
* '''Ponente:''' {{garanda}} (Grupo de Lógica Computacional - Universidad de Huelva)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Introducción a la teoría de la relatividad especial.
 +
 
 +
=== <span id="12-Dic-12">Seminario del 12 de diciembre de 2012</span> ===
 +
* '''Título:''' ''Lógicas temporales y Model Checking'' (3)
 +
* '''Ponente:''' {{fmartin}} (Grupo de Lógica Computacional - Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Tercera y última sesión dedidada a hacer una breve presentación sobre lógicas temporales. Hoy presentaremos dos algoritmos de Model-Checking, uno para cada una de las dos lógicas presentadas en la sesión anterior.
 +
 
 +
=== <span id="28-Nov-12">Seminario del 28 de noviembre de 2012</span> ===
 +
* '''Título:''' ''Turing-Taylor expansions of arithmetic theories''
 +
* '''Ponente:''' [http://www.phil.uu.nl/~jjoosten Joost J. Joosten] (Universidad de Barcelona)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:30 a 11:30.
 +
* '''Resumen:''' Well behaved real-valued functions can be assigned a converging Taylor expansion. In analogy we shall see that well-behaved arithmetic theories can be assigned what we call a converging Turing-Taylor expansion. The terms Xⁿ in the Taylor expansion are replaced by different kind of reflection principles. We shall see how various well-known sub-theories of Peano Arithmetic fit this framework and can be embedded in Ignatiev's model. This is slightly surprising since Ignatiev's model is a combinatoric structure motivated purely by modal logics. Moreover, we shall speak on how these expansions relate to ordinal analysis.
 +
 
 +
----
 +
 
 +
=== <span id="21-Nov-12">Seminario del 21 de noviembre de 2012</span> ===
 +
* '''Título:''' ''Lógicas temporales y Model Checking'' (2)
 +
* '''Ponente:''' {{fmartin}} (Grupo de Lógica Computacional - Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Segunda sesión dedidada a hacer una breve presentación sobre lógicas temporales. Hoy presentaremos las lógicas temporales LTL y CTL y analizaremos sus diferencias.
 +
 
 +
----
 +
 
 +
=== <span id="7-Nov-12">Seminario del 7 de noviembre de 2012</span> ===
 +
* '''Título:''' ''Lógicas temporales y Model Checking'' (1)
 +
* '''Ponente:''' {{fmartin}} (Grupo de Lógica Computacional - Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Esta es la primera sesión de un conjunto de varias dedicadas a realizar una breve presentación sobre lógicas temporales, su uso para establecer propiedades de sistemas de transición y los algoritmos que se utilizan para ello.
 +
 
 +
----
 +
 
 +
=== <span id="31-Oct-12">Seminario del 31 de octubre de 2012</span> ===
 +
* '''Título:''' ''La lógica de la demostrabilidad (Parte 3: Teorema de Solovay)''
 +
* '''Ponente:''' [http://personal.us.es/dfduque David Fernández Duque] (Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' En la sesión final de la serie sobre [http://plato.stanford.edu/entries/logic-provability/ lógica de la demostrabilidad] hablaremos de la completud de la [http://planetmath.org/ModalLogicGL.html la lógica GL] para su [http://plato.stanford.edu/entries/logic-provability/#4 interpretación aritmética], un teorema originalmente demostrado por Solovay en 1976. Utilizaremos técnicas vistas en las dos sesiones anteriores.
 +
* '''Referencias:''' En esta sesión cubriremos el capítulo 9 del libro deG. S. Boolos [http://goo.gl/wIL5m The Logic of Provability]. (Cambridge University Press, 1993). Las transparencias de este tema se pueden encontrar en los siguientes enlaces:
 +
** D. Fernández Duque y J.J. Joosten [http://www.phil.uu.nl/~jjoosten/events/ESSLLI2012/CourseMaterial/ESSLLITutorialDay2a.pdf Provability logics and applications. (Day 2a: Completeness results for GL)]
 +
** D. Fernández Duque y J.J. Joosten [http://www.phil.uu.nl/~jjoosten/events/ESSLLI2012/CourseMaterial/Day2b.pdf Provability logics and applications. (Day 2b: Completeness results for GL)]
 +
 
 +
----
 +
 
 +
=== <span id="24-Oct-12">Seminario del 24 de octubre de 2012</span> ===
 +
* '''Título:''' ''La lógica de la demostrabilidad (Parte 2: Semántica de mundos posibles)''
 +
* '''Ponente:''' [http://personal.us.es/dfduque David Fernández Duque] (Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' En esta segunda sesión de la serie sobre [http://plato.stanford.edu/entries/logic-provability/ lógica de la demostrabilidad] discutiremos la [http://plato.stanford.edu/entries/logic-provability/#3 semántica de mundos posibles] y la completud de [http://planetmath.org/ModalLogicGL.html la lógica GL] para esta interpretación. Daremos una breve introducción a la [http://plato.stanford.edu/entries/logic-provability/#3.4 semántica topológica] de la lógica modal.
 +
* '''Referencias:''' En esta sesión cubriremos los capítulos 4-7 del libro deG. S. Boolos [http://goo.gl/wIL5m The Logic of Provability]. (Cambridge University Press, 1993).
 +
 
 +
----
 +
 
 +
=== <span id="17-Oct-12">Seminario del 17 de octubre de 2012</span> ===
 +
* '''Título:''' ''La lógica de la demostrabilidad (Parte 1: Representación modal de la demostrabilidad)''
 +
* '''Ponente:''' [http://personal.us.es/dfduque David Fernández Duque] (Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' En la primera sesión del tutorial sobre lógica de la demostrabilidad haremos un repaso del segundo teorema de Gödel así como el teorema de Löb, y discutiremos su representación dentro de la lógica modal proposicional. Además, demostraremos la corrección del cálculo deductivo GL (de Gödel y Löb).
 +
* '''Referencias:''' En esta primera sesión cubriremos los capítulos 1-3 del libro de G. S. Boolos [http://goo.gl/wIL5m The Logic of Provability]. (Cambridge University Press, 1993). También contiene un material muy parecido las siguientes transparencias:
 +
** D. Fernández Duque y J.J. Joosten [http://www.phil.uu.nl/~jjoosten/events/ESSLLI2012/CourseMaterial/Day1a.pdf Provability logics and applications. (Day 1a: Provability as modality)]
 +
** D. Fernández Duque y J.J. Joosten [http://www.phil.uu.nl/~jjoosten/events/ESSLLI2012/CourseMaterial/ESSLLITutorialDay1b.pdf Provability logics and applications. (Day 1b: Provability as modality)]
 +
 
 +
----
 +
 
 +
=== <span id="17-Oct-12">Seminario del 9 de octubre de 2012</span> ===
 +
* '''Título:''' ''Experiencia en Proyectos de Simulación de crecimiento urbano''
 +
* '''Ponente:''' [http://carolcanter.weebly.com/ Carolina de Carvalho Cantergian] (Universidad de Alcalá de Henares)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 11:00 a 12:00.
 +
* '''Resumen:''' Presentación de los trabajos realizados, en el ámbito de la simulación urbana por el grupo de investigación al que pertenece, y futuras líneas de investigación.
 +
 
 +
----
 +
 
 +
=== <span id="24-Nov-11">Seminario del 24 de Noviembre de 2011</span> ===
 +
* '''Título:''' ''Razonamiento formalizado sobre formas normales proposicionales''
 +
* '''Ponente:''' ''Fabián F. Serrano Suárez'' (Universidad Nacional de Colombia)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:00 a 13:00.
 +
* '''Resumen:''' En esta sesión se presenta una formalización en Isabelle/HOL/Isar del algoritmo para el cálculo de formas normales conjuntivas presentado en el libro [http://bit.ly/shoulS First-order logic and automated theorem proving] de Melvin Fitting. Se demuestra en Isabelle la terminación y corrección del algoritmo.
 +
 
 +
----
 +
 
 +
=== <span id="27-Oct-11">Seminario del 27 de Octubre de 2011</span> ===
 +
* '''Título:''' ''Aplicaciones de la inteligencia artificial en las empresas''
 +
* '''Ponente:''' ''Joaquín Borrego Díaz'' (Universidad de Sevilla)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:00 a 13:00.
 +
* '''Resumen:''' En esta sesión se comentan los retos y oportunidades de I+D+i de la inteligencia artificial con empresas.
 +
 
 +
----
 +
 
 +
=== <span id="17-Nov-11">Seminario del 17 de Noviembre de 2011</span> ===
 +
* '''Título:''' ''Formalización en Isabelle de un cálculo axiomático de la lógica proposicional''
 +
* '''Ponente:''' ''Fabián F. Serrano Suárez'' (Universidad Nacional de Colombia)
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 12:00 a 13:00.
 +
* '''Resumen:''' En esta sesión se presenta una formalización en Isabelle/HOL/Isar de un sistema axiomático de la lógica proposicional basada en el libro de Mendelson. El objetivo es explorar la posibilidad de formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas.
 +
 
 +
----
 +
 
 +
=== Seminario del 18 de Octubre de 2011 ===
 +
* '''Título:''' ''Introducción a los sistemas complejos''
 +
* '''Ponente:''' ''Juan Carlos García Vázquez'' (Universidad de Sevilla).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:00 a 12:00.
 +
* '''Resumen:'''
 +
 
 +
----
 +
 
 +
=== Seminario del 11 de Octubre de 2011 ===
 +
* '''Título:''' ''Análisis formal de conceptos: aplicaciones''
 +
* '''Ponente:''' ''Juan Galán Páez'' (Universidad de Sevilla).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:00 a 11:30.
 +
* '''Resumen:'''
 +
 
 +
----
 +
 
 +
=== Seminario del 4 de Octubre de 2011 ===
 +
* '''Título:''' ''Introducción al análisis formal de conceptos''
 +
* '''Ponente:''' ''Juan Galán Páez'' (Universidad de Sevilla).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:00 a 11:30.
 +
* '''Resumen:'''
 +
 
 +
----
 +
 
 +
=== Seminario del 13 de Julio de 2011 ===
 +
* '''Título:''' ''Matrices de incidencia de complejos simpliciales en Coq/SSReflect/''
 +
* '''Ponente:''' ''Jónathan Heras Vicente'' (Departamento de Matemáticas y Computación de la Universidad de La Rioja).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:30 a 11:30.
 +
* '''Resumen:''' Los complejos simpliciales son una herramienta fundamental en la Topología Algebraica Computacional, ya que proporcionan una descripción elemental de objetos finitos. La teoría de complejos simpliciales se usa en distintos contextos como la teoría de códigos, la robótica o el análisis de imágenes digitales. En esta charla se presenta una formalización en Coq de los complejos simpliciales, sus matrices de incidencia así como el principal teorema que da sentido a la definición de grupos de homología y los primeros pasos hacia su cálculo.
 +
 
 +
----
 +
 
 +
=== Seminario del 20 de Octubre de 2010 ===
 +
* La sesión de esta semana se sustituye por las conferencias del [http://www.glc.us.es/cla2010 CLA 2010]
 +
 
 +
----
 +
 
 +
=== Seminario del 13 de Octubre de 2010 ===
 +
* '''Título:''' ''Social Ontology Documentation for Knowledge Externalization''
 +
* '''Ponente:''' ''Antonio J. Jimenez Mavillard'' (Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla).
 +
* '''Lugar:''' Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
 +
* '''Hora:''' De 10:30 a 11:30.
 +
* '''Resumen:''' Knowledge externalization and organization is a major challenge that companies must face. Also, they have to ask whether is possible to enhance its management. Mechanical processing of information represents a chance to carry out these tasks, as well as to turn intangible knowledge assets into real assets. Machine-readable knowledge provides a basis to enhance knowledge management. A promising approach is the empowering of Knowledge Externalization by the community (users, employees). In this talk, a social semantic tool (called OntoxicWiki) for enhancing the quality of knowledge is presented
  
−
== Sesiones previstas del seminario y anteriores ==
+
----
  
−
=== Seminario del 18 de Junio de 2010 ===
+
=== <span id="18-Jun-10">Seminario del 18 de Junio de 2010</span> ===
 +
[[image:munoz.png | right |thumb| 180px |Anuncio]] 
 
* '''Título:''' ''A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems''
 
* '''Título:''' ''A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems''
 
* '''Ponente:''' ''[http://shemesh.larc.nasa.gov/people/cam/ César A. Muñoz. NASA Langley Research Center, USA].''
 
* '''Ponente:''' ''[http://shemesh.larc.nasa.gov/people/cam/ César A. Muñoz. NASA Langley Research Center, USA].''
Línea 14: Línea 316:
 
* '''Hora:''' 11:30
 
* '''Hora:''' 11:30
 
* '''Resumen:''' In order to accommodate the predicted increase in air traffic operations over the next decades, the next generation of air transportation systems rely on new operational concepts where the responsibility for traffic separation is air/ground distributed. These new concepts will require an unprecedented level of safety-critical systems.State-based distributed Separation Assurance (SA) is one of such concepts and it refers to conflict prevention, detection, and resolution systems that rely exclusively on the state information, i.e., 3-D position and velocity vectors, that is broadcast by each aircraft. This talk presents the Airborne Coordinated Conflict Resolution and Detection (ACCoRD) framework for the design and verification of state-based separation assurance systems. The framework, which has been specified and mechanically verified in PVS, consists of a set of definitions and formally proven criteria that guarantee the correctness of a family of SA algorithms. For instance, in the case of pairwise conflict resolution, ACCoRD provides criteria that guarantee that two distributed algorithms, which satisfy the same coordination criteria, independently compute resolution maneuvers that yield conflict free trajectories when simultaneously implemented by the aircraft. This talk gives more examples of such criteria and algorithms that satisfy them. It also argues that a criteria-based verification framework, such as ACCoRD, will enable the natural evolution of the worldwide Air Transportation System.
 
* '''Resumen:''' In order to accommodate the predicted increase in air traffic operations over the next decades, the next generation of air transportation systems rely on new operational concepts where the responsibility for traffic separation is air/ground distributed. These new concepts will require an unprecedented level of safety-critical systems.State-based distributed Separation Assurance (SA) is one of such concepts and it refers to conflict prevention, detection, and resolution systems that rely exclusively on the state information, i.e., 3-D position and velocity vectors, that is broadcast by each aircraft. This talk presents the Airborne Coordinated Conflict Resolution and Detection (ACCoRD) framework for the design and verification of state-based separation assurance systems. The framework, which has been specified and mechanically verified in PVS, consists of a set of definitions and formally proven criteria that guarantee the correctness of a family of SA algorithms. For instance, in the case of pairwise conflict resolution, ACCoRD provides criteria that guarantee that two distributed algorithms, which satisfy the same coordination criteria, independently compute resolution maneuvers that yield conflict free trajectories when simultaneously implemented by the aircraft. This talk gives more examples of such criteria and algorithms that satisfy them. It also argues that a criteria-based verification framework, such as ACCoRD, will enable the natural evolution of the worldwide Air Transportation System.
−
[[image:munoz.png | right |thumb| 110px |Anuncio]] 
+
 
 
----
 
----
  
Línea 229: Línea 531:
 
<br> (Dicho Zen).
 
<br> (Dicho Zen).
 
</div>
 
</div>
 +
 +
 +
[[image:Sello-us.jpg]]
 +
* 'UNIVERSIDAD DE SEVILLA. VICERRECTORADO DE RELACIONES INSTITUCIONALES'
 +
** 'Las actividades de este seminario han sido financiadas parcialmente con una ayuda de Extensión universitaria de la Universidad de Sevilla'
  
 
[[Category: Seminario]]
 
[[Category: Seminario]]

Revisión actual del 22:46 1 abr 2017

Los Seminarios del Grupo de Lógica Computacional se celebrarán en el seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial. Las sesiones son abiertas y pueden acudir todas las personas interesadas.

Próximas sesiones del seminario

Seminario del 5 de abril de 2017

  • Título: Diseño de una plataforma para simulación de dispositivos inalámbricos
  • Ponente: Gonzalo A. Aranda-Corral (Grupo de Lógica Computacional - Universidad de Huelva).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:30 a 12:30.
  • Resumen: Aplicación de la tecnología multiagente JADE para la construcción de una plataforma de simulación de dispositivos inalámbricos.

Sesiones anteriores del seminario

Seminario del 30 de marzo de 2016

  • Título: Introducción a ROS con Deep Learning Robot
  • Ponente: Diego R. Cabrera Mendieta (Universidad Politécnica Salesiana, Ecuador).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:15 a 12:15.
  • Resumen: Las aplicaciones de la Inteligencia Artificial a la robótica están revolucionando el mundo actual. El comportamiento de los robots cada vez presenta más características "inteligentes". En este seminario vamos a ver distintas aplicaciones de inteligencia artificial ejecutadas sobre la plataforma Deep Learning Robot y programadas usando como framework base el sistema operativo para robots (ROS).

Seminario del 10 de febrero de 2016

  • Título: Buscando un modelo: lógicas modales, semántica y decibilidad
  • Ponente: Guillaume Hoffmann (Universidad Nacional de Córdoba, Argentina).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:15 a 12:15.
  • Resumen: En términos de expresividad y de comportamiento computacional, la lógicas modales están ubicadas entre la lógica proposicional y la lógica del primer orden. En esta charla vamos a ver porqué, y técnicas para demostrar la decibilidad o indecibilidad de una lógica: métodos de tableros y reducciones.

Seminario del 17 de diciembre de 2015

  • Título: Darcs: control de versiones para principiantes
  • Ponente: Guillaume Hoffmann (Universidad Nacional de Córdoba, Argentina).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 16:30 a 18:30.
  • Resumen: En el área del desarrollo de software, el control de versiones permite agilizar muchas tareas rutinarias. Involucra un software que ayuda al programador a guardar las distintas versiones de un software en desarrollo, y hacer ciertas operaciones sobres esas.

    En esta charla presentaré el software Darcs. Darcs es un sistema de control de versiones distribuido, libre y escrito en Haskell. Darcs es amigable: tiene un modelo de funcionamento accesible para usuarios inexpertos. Compararé Darcs con otros SCV (Git y Subversion) y presentaré unas ideas de proyectos que pueden interesar a estudiantes de informática.

    Ver también: Darcs en Sevilla.

Seminario del 16 de diciembre de 2015

  • Título: Darcs: un sistema de control de versiones distribuido
  • Ponente: Guillaume Hoffmann (Universidad Nacional de Córdoba, Argentina).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:15 a 12:15.
  • Resumen: Darcs es un sistema de control de versiones distribuido con un énfasis en la verificación de la corrección (utilizando Haskell y QuickCheck). En el seminario se explicará el uso y fundamento de Darcs.
    Más información en Darcs en Sevilla.

Seminario del 19 de junio de 2015

  • Título: Structure and Real-world SAT Solving
  • Ponente: Jesús Giráldez Crú (Artificial Intelligence Research Institute IIIA-CSIC, Barcelona).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:30 a 12:30.
  • Resumen: The Boolean Satisfiability problem (SAT) is the first known NP-complete problem. Besides its complexity, it is extensively used to solve practical applications (such as planning, scheduling or formal verification, among others). Modern SAT solvers have experienced a remarkable progress on solving these industrial (or real-world) SAT instances. Most of the techniques have been developed after an intensive experimental testing process. The common wisdom in the SAT community is that the success of these techniques is because they exploit some kind of hidden structure that industrial formulas actually have. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them.
    In this talk, we analyze some structural properties of SAT instances, viewed as graphs. Namely, they are the scale-free structure, the community structure and the self-similar structure. In addition, we explore how these graph properties are affected during SAT solving by effects of variable instantiation or clause learning. Finally, we present some applications in SAT solving based on these notions of structure.

Seminario del 29 de abril de 2015

  • Título: Enumeración de los racionales
  • Ponente: David Argullo
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: El código comentado correspondiente a la charla se encuentra en esta página.

Seminario del 15 de abril de 2015

  • Título: Los teoremas de incompletitud de Gödel
  • Ponente: Xavier Seguí
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: El objetivo del seminario es presentar los dos teoremas de incompletitud de Kurt Gödel, dando una visión conceptual de ellos. Dado que son dos de los resultados más profundos y paradójicos de la lógica matemática, se verá alguna aplicación tanto dentro como fuera del ámbito matemático.

Seminario del 11 de marzo de 2015

  • Título: El algoritmo de Huffmann en Isabelle/HOL
  • Ponente: David Rasero
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: El algoritmo de Huffman es un algoritmo para la codificación de datos, desarrollado por David A. Huffman en 1952. El objetivo del seminario es describir el algoritmo y esbozar una prueba formal de la corrección de este algoritmo, usando Isabelle/HOL.

Seminario del 18 de marzo de 2015

  • Título: El algoritmo de unificación.
  • Ponente: María Barranca
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: El objetivo del seminario es describir el algoritmo de unificación y esbozar una formalización del mismo en Isabelle/HOL.

Seminario del 4 de marzo de 2015

  • Título: Un algoritmo en tiempo lineal para construir un árbol de altura mínima (2ª parte)
  • Ponente: Daniel Rodríguez
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: Consideramos el problema de construir un árbol de altura mínima, cuya frontera sea una lista dada. Se analizan dos algoritmos, uno de ellos recursivo (o top-down) y el otro iterativo (o bottom-up). Aunque se obtienen árboles diferentes, ambos pueden implementarse en tiempo lineal en Haskell.

Seminario del 25 de febrero de 2015

  • Título: Un algoritmo en tiempo lineal para construir un árbol de altura mínima
  • Ponente: Daniel Rodríguez
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:45 a 11:30.
  • Resumen: Consideramos el problema de construir un árbol de altura mínima, cuya frontera sea una lista dada. Se analizan dos algoritmos, uno de ellos recursivo (o top-down) y el otro iterativo (o bottom-up). Aunque se obtienen árboles diferentes, ambos pueden implementarse en tiempo lineal en Haskell.

Seminario del 18 de febrero de 2015

  • Título: Algoritmo en tiempo lineal para buscar el menor objeto no usado
  • Ponente: Javier Rodríguez
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Un problema frecuente en programación es, dado un conjunto de objetos en uso, encontrar el menor objeto que no se está usando, entre todos los objetos susceptibles de ser usados. En esta sesión se describirán dos soluciones al problema en tiempo lineal y sus implementaciones en Haskell.

Seminario del 11 de febrero de 2015

  • Título: Perlas de programación funcional
  • Ponente: María José Hidalgo
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Hoy se inicia una serie de sesiones dedicadas a la exposición de "Perlas de programación funcional", basadas en:

Seminario del 3 de marzo de 2014

  • Título: Presentación de Terms
  • Ponente: Enrique Pérez Arnaud
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 17:00 a 18:00.
  • Resumen: Terms es un sistema basado en reglas, capaz de mantener bases de conocimiento persistentes, y de extraer deducciones de las mismas. El lenguaje en el que se expresa el conocimiento (reglas y hechos) es original del sistema, está basado en una teoría de primer orden, y está diseñado para expresar con sencillez el mismo tipo de conocimiento que se expresa normalmente con el lenguaje natural.

Seminario del 29 de enero de 2014

  • Título: Laboratorio de Sistemas Multiagente con JADE
  • Ponente: Gonzalo A. Aranda Corral
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 12:30.
  • Resumen: En esta sesión se realizará una introducción práctica a la plataforma JADE para sistemas multiagente

Seminario del 27 de noviembre de 2013

  • Título: Formalización de la prueba de la trascendencia del número e
  • Ponente: Pedro G. Ros Reina
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:30 a 13:30.
  • Resumen: En la charla se explicará la prueba de Hermite de que el número e es trascendente y la formalización de Jesse Bingham en HOL Light.

Seminario del 16 de octubre de 2013

  • Título: Desarrollo colaborativo de programas: Git
  • Ponente: Pedro Almagro Blanco
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:30 a 13:30.
  • Resumen: Introducción al desarrollo de software de forma colaborativa usando como soporte la plataforma Git.

Seminario del 16 de mayo de 2013

  • Título: Formalización de la Relatividad (especial) en lógica de primer orden. Parte II
  • Ponente: Gonzalo A. Aranda-Corral (Grupo de Lógica Computacional - Universidad de Huelva)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 13:00.
  • Resumen: En esta charla se continuará con la formalización de la RE, terminando con la demostración de un teorema.

Seminario del 11 de abril de 2013

  • Título: Formalización de la Relatividad (especial) en lógica de primer orden. Introducción
  • Ponente: Gonzalo A. Aranda-Corral (Grupo de Lógica Computacional - Universidad de Huelva)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: En esta charla se comenzará la formalización de la Relatividad Especial(RE), estableciendo las bases de la representación del conocimiento y traduciendo los axiomas de la RE en enunciados lógicos.

Seminario del 16 de enero de 2013

  • Título: Relatividad (especial)
  • Ponente: Gonzalo A. Aranda-Corral (Grupo de Lógica Computacional - Universidad de Huelva)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Introducción a la teoría de la relatividad especial.

Seminario del 12 de diciembre de 2012

  • Título: Lógicas temporales y Model Checking (3)
  • Ponente: Francisco J. Martín (Grupo de Lógica Computacional - Universidad de Sevilla)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Tercera y última sesión dedidada a hacer una breve presentación sobre lógicas temporales. Hoy presentaremos dos algoritmos de Model-Checking, uno para cada una de las dos lógicas presentadas en la sesión anterior.

Seminario del 28 de noviembre de 2012

  • Título: Turing-Taylor expansions of arithmetic theories
  • Ponente: Joost J. Joosten (Universidad de Barcelona)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: Well behaved real-valued functions can be assigned a converging Taylor expansion. In analogy we shall see that well-behaved arithmetic theories can be assigned what we call a converging Turing-Taylor expansion. The terms Xⁿ in the Taylor expansion are replaced by different kind of reflection principles. We shall see how various well-known sub-theories of Peano Arithmetic fit this framework and can be embedded in Ignatiev's model. This is slightly surprising since Ignatiev's model is a combinatoric structure motivated purely by modal logics. Moreover, we shall speak on how these expansions relate to ordinal analysis.

Seminario del 21 de noviembre de 2012

  • Título: Lógicas temporales y Model Checking (2)
  • Ponente: Francisco J. Martín (Grupo de Lógica Computacional - Universidad de Sevilla)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Segunda sesión dedidada a hacer una breve presentación sobre lógicas temporales. Hoy presentaremos las lógicas temporales LTL y CTL y analizaremos sus diferencias.

Seminario del 7 de noviembre de 2012

  • Título: Lógicas temporales y Model Checking (1)
  • Ponente: Francisco J. Martín (Grupo de Lógica Computacional - Universidad de Sevilla)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Esta es la primera sesión de un conjunto de varias dedicadas a realizar una breve presentación sobre lógicas temporales, su uso para establecer propiedades de sistemas de transición y los algoritmos que se utilizan para ello.

Seminario del 31 de octubre de 2012

Seminario del 24 de octubre de 2012

Seminario del 17 de octubre de 2012

  • Título: La lógica de la demostrabilidad (Parte 1: Representación modal de la demostrabilidad)
  • Ponente: David Fernández Duque (Universidad de Sevilla)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: En la primera sesión del tutorial sobre lógica de la demostrabilidad haremos un repaso del segundo teorema de Gödel así como el teorema de Löb, y discutiremos su representación dentro de la lógica modal proposicional. Además, demostraremos la corrección del cálculo deductivo GL (de Gödel y Löb).
  • Referencias: En esta primera sesión cubriremos los capítulos 1-3 del libro de G. S. Boolos The Logic of Provability. (Cambridge University Press, 1993). También contiene un material muy parecido las siguientes transparencias:

Seminario del 9 de octubre de 2012

  • Título: Experiencia en Proyectos de Simulación de crecimiento urbano
  • Ponente: Carolina de Carvalho Cantergian (Universidad de Alcalá de Henares)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 11:00 a 12:00.
  • Resumen: Presentación de los trabajos realizados, en el ámbito de la simulación urbana por el grupo de investigación al que pertenece, y futuras líneas de investigación.

Seminario del 24 de Noviembre de 2011

  • Título: Razonamiento formalizado sobre formas normales proposicionales
  • Ponente: Fabián F. Serrano Suárez (Universidad Nacional de Colombia)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 13:00.
  • Resumen: En esta sesión se presenta una formalización en Isabelle/HOL/Isar del algoritmo para el cálculo de formas normales conjuntivas presentado en el libro First-order logic and automated theorem proving de Melvin Fitting. Se demuestra en Isabelle la terminación y corrección del algoritmo.

Seminario del 27 de Octubre de 2011

  • Título: Aplicaciones de la inteligencia artificial en las empresas
  • Ponente: Joaquín Borrego Díaz (Universidad de Sevilla)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 13:00.
  • Resumen: En esta sesión se comentan los retos y oportunidades de I+D+i de la inteligencia artificial con empresas.

Seminario del 17 de Noviembre de 2011

  • Título: Formalización en Isabelle de un cálculo axiomático de la lógica proposicional
  • Ponente: Fabián F. Serrano Suárez (Universidad Nacional de Colombia)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 13:00.
  • Resumen: En esta sesión se presenta una formalización en Isabelle/HOL/Isar de un sistema axiomático de la lógica proposicional basada en el libro de Mendelson. El objetivo es explorar la posibilidad de formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas.

Seminario del 18 de Octubre de 2011

  • Título: Introducción a los sistemas complejos
  • Ponente: Juan Carlos García Vázquez (Universidad de Sevilla).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:00 a 12:00.
  • Resumen:

Seminario del 11 de Octubre de 2011

  • Título: Análisis formal de conceptos: aplicaciones
  • Ponente: Juan Galán Páez (Universidad de Sevilla).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:00 a 11:30.
  • Resumen:

Seminario del 4 de Octubre de 2011

  • Título: Introducción al análisis formal de conceptos
  • Ponente: Juan Galán Páez (Universidad de Sevilla).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:00 a 11:30.
  • Resumen:

Seminario del 13 de Julio de 2011

  • Título: Matrices de incidencia de complejos simpliciales en Coq/SSReflect/
  • Ponente: Jónathan Heras Vicente (Departamento de Matemáticas y Computación de la Universidad de La Rioja).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: Los complejos simpliciales son una herramienta fundamental en la Topología Algebraica Computacional, ya que proporcionan una descripción elemental de objetos finitos. La teoría de complejos simpliciales se usa en distintos contextos como la teoría de códigos, la robótica o el análisis de imágenes digitales. En esta charla se presenta una formalización en Coq de los complejos simpliciales, sus matrices de incidencia así como el principal teorema que da sentido a la definición de grupos de homología y los primeros pasos hacia su cálculo.

Seminario del 20 de Octubre de 2010

  • La sesión de esta semana se sustituye por las conferencias del CLA 2010

Seminario del 13 de Octubre de 2010

  • Título: Social Ontology Documentation for Knowledge Externalization
  • Ponente: Antonio J. Jimenez Mavillard (Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla).
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: Knowledge externalization and organization is a major challenge that companies must face. Also, they have to ask whether is possible to enhance its management. Mechanical processing of information represents a chance to carry out these tasks, as well as to turn intangible knowledge assets into real assets. Machine-readable knowledge provides a basis to enhance knowledge management. A promising approach is the empowering of Knowledge Externalization by the community (users, employees). In this talk, a social semantic tool (called OntoxicWiki) for enhancing the quality of knowledge is presented

Seminario del 18 de Junio de 2010

Error al crear miniatura: No se ha podido guardar la miniatura
Anuncio
  • Título: A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems
  • Ponente: César A. Muñoz. NASA Langley Research Center, USA.
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: 11:30
  • Resumen: In order to accommodate the predicted increase in air traffic operations over the next decades, the next generation of air transportation systems rely on new operational concepts where the responsibility for traffic separation is air/ground distributed. These new concepts will require an unprecedented level of safety-critical systems.State-based distributed Separation Assurance (SA) is one of such concepts and it refers to conflict prevention, detection, and resolution systems that rely exclusively on the state information, i.e., 3-D position and velocity vectors, that is broadcast by each aircraft. This talk presents the Airborne Coordinated Conflict Resolution and Detection (ACCoRD) framework for the design and verification of state-based separation assurance systems. The framework, which has been specified and mechanically verified in PVS, consists of a set of definitions and formally proven criteria that guarantee the correctness of a family of SA algorithms. For instance, in the case of pairwise conflict resolution, ACCoRD provides criteria that guarantee that two distributed algorithms, which satisfy the same coordination criteria, independently compute resolution maneuvers that yield conflict free trajectories when simultaneously implemented by the aircraft. This talk gives more examples of such criteria and algorithms that satisfy them. It also argues that a criteria-based verification framework, such as ACCoRD, will enable the natural evolution of the worldwide Air Transportation System.

Seminario del 18 de Mayo de 2010

  • Título: JADE: Una plataforma para sistemas multiagente (II)
  • Ponente: Gonzalo A. Aranda Corral, Universidad de Huelva. Departmento de Tecnologías de la Información.
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 14:00.
  • Resumen: En esta continuación del seminario anterior se presentarán ejemplos de programación en JADE de sistemas multiagente

Seminario del 11 de Mayo de 2010

  • Título: JADE: Una plataforma para sistemas multiagente (I)
  • Ponente: Gonzalo A. Aranda Corral, Universidad de Huelva. Departmento de Tecnologías de la Información.
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 12:00 a 14:00.
  • Resumen: Se introducirá la plataforma JADE como herramienta para la programación de sistemas multiagente

Seminario del 18 de Marzo de 2010

  • Título: Objetos digitales educativos
  • Ponente: Jesús Peñas Cano (Instituto online de Andalucía)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 18:30 a 20:30.
  • Resumen: Se introducirá el concepto de "objeto digital educativo", su especificación, estándares, propiedades principales, arquitectura, propiedades de agregación, etc.

Seminario del 11 de Marzo de 2010

  • Título: Diferentes usos de las TIC en el área de matemáticas (II)
  • Ponente: José Muñoz Santoja (Instituto online de Andalucía)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 18:30 a 20:30.
  • Resumen: En la charla se tratará la integración de competencias en tareas matemáticas así como en la formalización y desarrollo de documentación asociada.

Seminario del 4 de Marzo de 2010

  • Título: Diferentes usos de las TIC en el área de matemáticas (I)
  • Ponente: Jesús Fernández Domínguez (Instituto online de Andalucía)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 18:30 a 20:30.
  • Resumen: En la charla se tratarán las nuevas herramientas TIC para la investigación educativa en matemáticas

Seminario del 25 de Febrero de 2010

  • Título: Enseñanza on-line en Andalucía: ESA y Bachillerato
  • Ponente: Juan José Muñoz Lorencio (Instituto online de Andalucía)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 18:30 a 20:30.
  • Resumen: En la charla se tratará la estructura de gestión del conocimiento con plataformas de e-learning para la enseñanza online en Andalucía, así como la innovación en el aprendizaje. Se mostrará como la Web 2.0 se ha usado como herramienta tecnológica para la aplicación de la inteligencia colectiva en la educación.

Seminario del 11 de Febrero de 2010

  • Título: fKenzo: a user interface for computations in Algebraic Topology
  • Ponente: Jónathan Heras (Universidad de La Rioja)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: fKenzo (= friendly Kenzo) is a graphical user interface providing a user-friendly front-end for the Kenzo system, a Common Lisp program devoted to Algebraic Topology. The fKenzo system provides the user interface itself, an XML intermediary generator-translator and, finally the Kenzo kernel. In this talk, the main points of fKenzo and the use of this system as a framework for interacting with Computer Algebra Systems and Theorem Provers related with Algebraic Topology are described.

Seminario del 19 de Noviembre de 2009

La sesión del día 19 se suspende, porque asistiremos a las II Jornadas de Lógica, Computación e Inteligencia Artificial.


Seminario del 12 de Noviembre de 2009

La sesión del día 12 se suspende, porque asistiremos al CLAI 2009 (Workshop on Computational Logics and Artificial Intelligence)

Seminario del 9 de Noviembre de 2009

  • Título: Retículos de T-conceptos multiadjuntos
  • Ponente: Manuel Ojeda (Universidad de Málaga)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: En la charla se describirá se introducirá el retículo de conceptos multiadjunto como un marco para integrar la lógica borrosa en el Análisis Formal de Conceptos.

Seminario del 5 de Noviembre de 2009

  • Título: Formalización de la topología simplicial
  • Ponente: Laureano Lambán (Universidad de La Rioja)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 10:30 a 11:30.
  • Resumen: Se propone un modelo, inspirado por la definición de los conjuntos simpliciales como prehaces, que permite desarrollar partes de la topología simplicial de un modo formal y bien adaptado a sistemas como ACL2. El objetivo que se persigue es reducir a lógica de primer orden definiciones y propiedades topológicas que, en su enunciado habitual, requieren orden superior. En el modelo, las pruebas se interpretan como pruebasde igualdad mediante reescritura en un anillo, el de los polinomios simpliciales.

Seminario del 29 de Octubre de 2009

  • Título: A logic for informative events
  • Ponente: Tim French (The University of Western Australia)
  • Lugar: Seminario del módulo E del Departamento de Ciencias de la Computación e Inteligencia Artificial.
  • Hora: De 13:00 a 14:00.
  • Resumen: Modal logic is frequently used for modelling knowledge in multi-agent systems. The semantics of modal logic uses the notion of possible worlds, between which an agent is unable to distinguish. In dynamic systems agents acquire new knowledge (say by an announcement, or the execution of some action) that allows to distinguish between worlds they previously could not separate. From the agents point of view, what were possible worlds become inconceivable. We introduce a multi-agent logic of knowledge with time where F phi stands for `there is an informative event after which phi'. Formula F phi is true in a model iff it is true in all its refinements (i.e., `atoms' and `back' are satisfied; the dual of simulation). We investigate a correspondence between these semantics and various other dynamic epistemic logics; show the resulting logic is decidable; and provide a sound and complete axiomatization for the logic.

Seminario del 22 de Octubre de 2009

  • Título: Formalización de la demostración de completitud de la lógica proposicional en Isabelle/Isar
  • Ponente: Fabián F. Serrano Suárez
  • Resumen: En esta sesión se presenta una formalización en Isabelle/HOL/Isar de un sistema axiomático de la lógica proposicional y la demostración de la completitud del sistema usando el método de Kalmar de eliminación de variables. La formalización se basa en la del libro de Mendelson. El objetivo es explorar la posibilidad de formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas.
  • Enlaces

Seminario del 20 de Mayo de 2009

  • Título: Panorama del razonamiento formalizado
  • Ponente: José A. Alonso
  • Resumen: Se presentará un panorama del trabajo realizado en el campo del razonamiento formalizado en los últimos 20 años y algunos retos planteados para su futuro desarrollo.

Seminario del 13 de Mayo de 2009

  • Título: Notas sobre el futuro de la búsqueda en la web
  • Ponente: Gonzalo A. Aranda-Corral
  • Resumen: Comentarios sobre las tendencias futuras de las búsquedas realizadas en la Web y cuales son los retos actuales a los que se están enfrentando los investigadores en estos momentos. Estas notas están extraídas de la asistencia al 4 workshop Future of Web Search: Semantic Search. También se incluirán algunas notas sobre la reunión del VoCamp 2009.

Seminario del 22 de Abril de 2009

  • Título: Un modelo algebraico de toma de decisiones para enclavamientos ferroviarios independiente de la topología de la estación
  • Ponente: Eugenio Roanes Lozano (Universidad Complutense de Madrid)
  • Resumen: Los enclavamientos ferroviarios son dispositivos que impiden el posicionar las agujas de los cambios de vía y abrir semáforos de modo que, en el peor caso, pueda darse una colisión. Es un problema relativamente similar al de verificación de sistemas expertos basados en reglas. Se presentará un modelo algebraico, indepedientemente de la topología de la estación, basado en el uso de bases de Groebner.

Seminario del 25 de Marzo de 2009

Seminario del 18 de Marzo de 2009

Seminario del 25 de Febrero de 2009

  • Título: Retracción conservativa de teorías proposicionales y su aplicación a los sistemas de clasificación
  • Ponente: Joaquín Borrego
  • Resumen: Se presenta una nueva regla para la lógica proposicional, denominada la regla de independencia que hemos diseñado para calcular la retracción conservativa de una base de conocimiento proposicional (y por tanto es aplicable a ontologías en lógica descriptiva proposicional). La regla está definida a partir de las derivadas booleanas en el anillo F2[x]. Describiremos las pruebas de adecuación y completitud del cálculo basado en esa regla así como otras aplicaciones de ésta, como: la localización de ontologías, la obtención de contextos maximales y la fusión jerárquica de ontologías mutuamente inconsistentes.

Seminario del 3 de Diciembre de 2008

Seminario del 26 de Noviembre de 2008

  • Título: Gestión y planificación de Proyectos de Investigación
  • Resumen: En esta se tratará cuestiones relativas a la gestión de los próximos proyectos nacionales de investigación. La sesión es restringida para los miembros del Grupo de Lógica Computacional participantes en los proyectos.

Seminario del 19 de Noviembre de 2008

  • Título: Elementos de Matemáticas formalizados en Isabelle/Isar
  • Ponente: Fabián F. Serrano Suárez
  • Resumen: Esta sesión del Seminario es una continuación de la presentación de métodos de construcción de pruebas formales y estructuradas en el lenguaje Isabelle/Isar. Su objetivo consiste en estudiar la analogía entre la prueba matemática (prueba informal) y la prueba semi-automática en Isar (prueba formal) de algunos resultados de las teorías básicas de las matemáticas.

Seminario del 12 de Noviembre de 2008

Seminario del 5 de Noviembre de 2008

  • Título: Mathserve: Web Semántica aplicada a Razonamiento Automático
  • Ponente: Héctor Fabián Echeverry Quintero
  • Resumen: Mathserve es un framework creado por Jürgen Zimmer que integra tecnologías de la Web Semántica con técnicas de Inteligencia Artificial aplicadas a Sistemas de Razonamiento Automático. En este seminario, se expondrán las características generales del mismo y sus posibles aplicaciones.
  • Enlaces:

Seminario del 29 de Octubre de 2008

  • Título: Programación visual con Pure Data
  • Ponente: Fernando Gómez
  • Resumen: Se presentará el entorno de programación visual en tiempo real Pure Data, conceptos básicos y posibles aplicaciones. Se trata de un lenguaje visual sencillo con un entorno de desarrollo Open Source y multiplaforma, interesante para proyectos fin de carrera. Inicialmente creado por Miller Puckette para la creación de programas de audio y performances, actualmente también es utilizado para la programación de prototipos y sistemas interactivos (aplicaciones que utilizan arduino, wiimote, ipod Touch, iphone).
  • Enlaces:

Seminario del 15 de Octubre de 2008

  • Título: La regla de independencia y su aplicación al aprendizaje de atributos
  • Ponente: Joaquín Borrego
  • Resumen: En esta charla presentaremos una nueva regla de inferencia, de carácter proposicicional (la regla de independencia). Se mostrará una aplicación de dicha regla al aprendizaje de atributos en el Análisis Formal de Conceptos

Seminarios anteriores

En esta sección se encuentran los seminarios de los cursos anteriores.

Material de interés para el Seminario del GLC

En esta sección se recoge una relación de materiales que sería interesante comentar en el Seminario.

Caminante, no hay camino:
se hace camino al andar.
(A. Machado)

Con cada paso que das alcanzas tu meta.
(Dicho Zen).


Error al crear miniatura: No se ha podido guardar la miniatura
  • 'UNIVERSIDAD DE SEVILLA. VICERRECTORADO DE RELACIONES INSTITUCIONALES'
    • 'Las actividades de este seminario han sido financiadas parcialmente con una ayuda de Extensión universitaria de la Universidad de Sevilla'
Obtenido de «https://www.glc.us.es/web/index.php?title=Seminario_del_Grupo_de_Lógica_Computacional&oldid=1291»