A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

A formalisation of Göodel’s incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows Świerczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of HF is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.

LI2013: Equivalencia de problemas proposicionales. Deducción natural

En la primera parte de la clase de hoy del curso Lógica Informática se ha demostrado la equivalencia de los siguientes problemas

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

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.

A formal model and correctness proof for an access control policy framework

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í.