Archivo de la categoría ‘Razonamiento Asistido por Computador’

RAC: trabajo final

En la página de la asignatura se ha publicado un listado de ejercicios que constituyen el trabajo final de la asignatura.

El plazo máximo de entrega de estos ejercicios es el día 20 de julio. Estoy a vuestra disposición para todas las consultas que queráis realizar, tanto en el despacho, como por correo o telefónicamente (954557883).

RAC: próximas clases del 13 y 16 de junio

La dos últimas clases se dedicarán a la realización de ejemplos concretos de verificación usando ACL2  Sedan. Los ejemplos se tomarán del capítulo 19 del libro “Computer Aided Reasoning: An Approach”.

Como ejercicio a entregar, se pide el bloque 8, antes del 19 de junio. Este ejercico es similar a la demostración de la corrección mergesort, pero usando la noción de “permutación”, en lugar de la de “ocurrencias”.

La semana que viene publicaré una serie de ejercicios que habrá que hacer como trabajo final de la asignatura.

RAC: próxima clase 9 de junio

Se recuerda que el próximo día 2 de junio no hay clase de RAC, y que esta clase queda aplazada para el día 13 de junio a la misma hora.

Para la clase del próximo 9 de junio, hay que realizar, en ACL2 Sedan, la demostración de que el algoritmo mergesort devuelve una lista ordenda.

RAC: clase del próximo 26 de mayo

En la próxima clase veremos el tema 6, en el que se explicará la manera de interactuar con el demostrador. Es conveniente que os llevéis vuestro ordenador con ACL2 Sedan, ya que haremos varias demostraciones prácticas, y sería mejor que las hicéramos entre todos.

También comentaré algunas cuestiones sobre los ejercicios de demostración a mano, para aquellos que quedan por entregarlo.

RAC: clase del próximo 19 de mayo

En la próxima clase, seguiremos hablando del demostrador automático de ACL2 (tema 5). En concreto, sobre las técnicas de simplificación e inducción que tiene implementadas.

En cuanto a la entrega prevista para mañana (bloque 6), ampliamos el plazo de entrega, hasta la semana que viene. Consultadme cualquier duda que tengáis en el desarrollo de las pruebas a mano y no la entreguéis hasta que estéis seguros de que está bien.