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.

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

Automation of mathematical induction as part of the history of logic

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.

The ontological argument in PVS

Se ha publicado un artículo de razonamiento formalizado en PVS titulado The ontological argument in PVS.

Su autor es John Rushby (del SRI International).

Su resumen es

The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in PVS and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.

Formalizing Moessner’s theorem and generalizations in Nuprl

Se ha publicado un artículo de razonamiento formalizado en Nuplr titulado Formalizing Moessner’s theorem and generalizations in Nuprl.

Sus autores son

Su resumen es

Moessner’s theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^n, 2^n, 3^n, \dots. Several generalizations of Moessner’s theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner’s original theorem and its known generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl. To the best of our knowledge, this is the first existing machine formalization. On the one hand, the formalization remains remarkably close to the original proof. On the other hand, it leads to new insights in the proof, pointing to small gaps and ambiguities that would never raise any objections in pen and pencil proofs, but which must be resolved in machine formalization.