En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 2ª relación (a partir del 9) sobre definiciones por composición de funciones sobre listas.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por composición de funciones sobre listas (2)”
En la primera parte de la clase de hoy del curso Lógica Informática se ha demostrado la equivalencia de los siguientes problemas
En la segunda parte hemos comenzado el estudio de la deducción natural proposicional. Las reglas que se han visto en la clase de hoy son las de la conjunción y de la doble negación.
Además, se ha comentado cómo formalizar en Isabelle/HOL la demostración del primer ejemplo, presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática. El código de las demostraciones se encuentran en la teoría del tema 3.
Finalmente, se han comentado las soluciones de la 3º relación de ejercicios.
Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL titulado A formal model and correctness proof for an access control policy framework.
Sus autores son
Su resumen es
If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model—a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security com- promise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson’s inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.
El trabajo se presentará en diciembre en el CPP 2013 (3rd Conference on Certified Programs and Proofs.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
El objetivo fundamental de la clase de hoy del curso Lógica Informáticaha consistido en responder estas dos preguntas:
Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursión. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).
Hemos continuado planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.
Además, se han definidos los conceptos de equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y la relación de consecuencia lógica.
Se ha visto la equivalencia de los siguientes problemas
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos.
También, se ha explicado cómo se puede usar en la resolución de los anteriores problemas el Gateway to Logic.
Finalmente, se han comentado las soluciones de la 2ª relación y cómo se puede usar APLI2 para comprobar la corrección de la formalización.
Las transparencias de esta clase son las páginas 14-34 del tema 1
Read More “LI2013: Semántica de la lógica proposicional”
Se ha publicado un artículo sobre la historia del razonamiento automático titulado Automation of mathematical induction as part of the history of logic.
Sus autores son
Su resumen es
We review the history of the automation of mathematical induction.
This article is further organized as follows.
§§ 4 and 5 offer a self-contained reference for the readers who are not familiar with the field of mathematical induction and its automation. In § 4 we introduce the essentials of mathematical induction. In § 5 we have to become more formal regarding recursive function definitions, their consistency, termination, and induction templates and schemes.
The main part is § 6, where we present the historically most important systems in automated induction, and discuss the details of software systems for explicit induction, with a focus on the 1970s. After describing the application context in § 6.1, we describe the following Boyer–Moore theorem provers: the Pure LISP Theorem Prover (§ 6.2) Thm (§ 6.3) Nqthm (§ 6.4), and ACL2 (§ 6.5). The most noteworthy remaining explicit- induction systems are sketched in § 6.6.
Alternative approaches to the automation of induction that do not follow the paradigm of explicit induction are discussed in § 7.
After summarizing the lessons learned in § 8, we conclude with § 9.