Seminários 2007.2

• 11/12/2007
  "Desarrollo formal de sistemas de software: lógica, álgebra y teoría de categorías en acción",
  por Prof. Carlos Lopez Pombo, Univ. de Buenos Aires (UBA), Argentina.
  
  Resumo:
  
  La matemática sufrió en el siglo pasado dos quiebres que determinaron, o debieran haberlo hecho, su caida de la segura torre de cristal del platonismo. El primero fue la demostración de imcompletitud de la aritmética (Gödel, 1931) y el segundo, fuertemente ligado al primero, fue la introducción de la noción de computabilidad (Turing, 1936). Este último hecho aporta una percepción de los programas y sus computaciones como objetos matemáticos que no sólo no escapan a su rigor y formalidad, sino que además proporciona la herramienta básica para la construcción de demostraciones de correctitud, muchas veces necesaria cuando un programa tiene un rol crítico y sus defectos pueden provocar enormes pérdidas, sean estas materiales (ej. sistemas de administración de transacciones bancarias, control de lineas de producción, etc.), o en el peor de los casos de vidas humanas (ej. control de vuelo de aviones, sistemas de control de centrales nucleares, etc.).
  
  Álgebra, lógica y teoría de categorías; son algunas de las herramientas de las que disponemos con el proveer descripciones formales de software.
  
  Los sistemas de software poseen aspectos muy diversos, por ejemplo estos tiene propiedades temporales, dinámicas y estáticas; y para cada uno de estos aspectos existen lenguajes lógicas que son capaces de capturarlos. Ahora, cómo se relacionan estas descripciones en lógicas diferentes? puede ocurrir que surjan contradicciones de aspectos diferentes de un mismo sistema? es posible que existan comportamientos que son consecuencia de aspectos diferentes y que no pueden ser descriptos por nunguno de ellos en forma aislada? En esta charla veremos cómo estas herramientas pueden ser combinadas para dar respuesta a estas y otras preguntas y así configurar una metodología para construir software correcto.
  
  
• 04/10/2007
  "A holding-your-hand presentation of the positive relational graph calculus - Part II",
  por Renata de Freitas, IM-UFF.
  Ver resumo em 27/09/2007.
  
  
• 27/09/2007
  "A holding-your-hand presentation of the positive relational graph calculus",
  por Renata de Freitas, IM-UFF.
  Resumo:
  The positive relational graph calculus is a graphical dedutive system that can be used to decide the valid inclusions between positive relational terms. We present the basics of this calculus by the exam of a series of examples, each one showing the purpose of a specific feature of the system.
  
  
• 23/08/2007 - excepcionalmente às 10h
  "Desenvolvimento de um Assistente de Construção de Provas em Dedução Natural",
  por Lucas de Andrade, bolsista IC-FAPERJ.
  Resumo:
  Serão apresentados os resultados obtidos até o momento, relacionados à especificação e concepção de um assistente de construção de provas em dedução natural para lógica proposicional, com foco no desenvolvimento de um ambiente interativo para edição de provas. Serão abordadas as etapas de fundamentação, análise do estado da arte e algumas etapas de desenvolvimento do sistema.
  Serão feitos comentários a respeito de alguns provadores e assistentes que estão disponíveis atualmente. Pretende-se não apenas explicitar algumas funcionalidades relevantes como também apontar os aspectos relativos às interfaces que necessitam de melhoria e inovação.
  Como resultado dessa análise já foi possível estabelecer alguns pontos críticos a serem levados em consideração durante o desenvolvimento do sistema e que podem também servir de base para a avaliação do resultado obtido na fase final do projeto.