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 verificación formal en ACL2 titulado Verified AIG algorithms in ACL2.
Sus autores son
Su resumen es
And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches.
We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms.
Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance
El trabajo se ha presentado en el ACL2 2013 (Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications).
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”