Hoy ha comenzado el curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.
En la clase de hoy se ha presentado la asignatura y se ha comentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.
Read More “RA2010: Visión panorámica del razonamiento automático”
EL 29 de Octubre se publicó un nuevo artículo de vrificación: Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming en la revista Science of Computer Programming.
Los autores del artículo son Kyungmin Bae (de la University de Illinois en Urbana-Champaign), Peter Csaba Olveczky (de la Universidad de Oslo), Thomas Huining Feng, Edward A. Lee y Stavros Tripakis (los tres últimos, de la Universidad de California en Berkeley).
El resumen del artículo es
This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.
Una versión previa del artículo, de libre acceso, es Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude.
El objetivo de la clase de hoy es aprender, resolviendo ejercicios, a definir funciones en Haskell usando las listas de comprensión introducidas en el tema 5.
En concreto, se han resuelto los siguientes ejercicios de la 5ª relación: 1 (sumaDeCuadrados), 2.1 (replica), 2.2 (prop_replica), 3.1 (pitagoricas), 4 (perfectos) y 8 (euler1).
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 6ª relación.
El objetivo del tema es aprender a definir funciones en Haskell usando listas de comprensión.
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 5ª relación.
Las transparencias usadas en la clase son las 10 primeras del tema 5
En la clase de hoy se ha realizado el primer examen de la evaluación continua.
Las notas se han publicado en la WebCT.
En la página de la asignatura se han publicado las soluciones del examen.
El resumen estadístico del resultado del examen es el siguiente
| No presentados | 11 | |
| Suspensos | 3 | 14.3% |
| Aprobados | 3 | 14.3% |
| Notables | 3 | 14.3% |
| Sobresalientes | 12 | 57.1% |
| Total | 32 |
El porcentaje de aprobados (sobre presentados) es 85.7 y la nota media es 8.1.