Isabelle

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle titulado Abstract interpretation of annotated commands.

Su autor es Tobias Nipkow (del Theorem Proving Group de la Technische Universität München).

El resumen del trabajo es

This paper formalises a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.

Las correspondientes teorías de Isabelle se encuentran aquí.

Se ha publicado un nuevo trabajo de razonamiento formalizado en Isabelle: Formalizing adequacy: A case study for higher-order abstract syntax.

Sus autores son James Cheney, Michael Norrish y René Vestergaard.

Su resumen es

Adequacy is an important criterion for judging whether a formalization is suitable for reasoning about the actual object of study. The issue is particularly subtle in the expansive case of approaches to languages with name-binding. In prior work, adequacy has been formalized only with respect to specific representation techniques. In this article, we give a general formal definition based on model-theoretic isomorphisms or interpretations. We investigate and formalize an adequate interpretation of untyped lambda-calculus within a higher-order metalanguage in Isabelle/HOL using the Nominal Datatype Package. Formalization elucidates some subtle issues that have been neglected in informal arguments concerning adequacy.

La formalización en Isabelle se encuentra aquí.

Se ha publicado en The Archive of Formal Proofs un nuevo trabajo de razonamiento formalizado en Isabelle sobre geometría: Proving the impossibility of trisecting an angle and doubling the cube.

Sus autors son Ralph Romanos y Lawrence Paulson (de la Universidad de Cambridge).

Su resumen es

Squaring the circle, doubling the cube and trisecting an angle, using a compass and straightedge alone, are classic unsolved problems first posed by the ancient Greeks. All three problems were proved to be impossible in the 19th century. The following document presents the proof of the impossibility of solving the latter two problems using Isabelle/HOL, following a proof by Carrega. The proof uses elementary methods: no Galois theory or field extensions. The set of points constructible using a compass and straightedge is defined inductively. Radical expressions, which involve only square roots and arithmetic of rational numbers, are defined, and we find that all constructive points have radical coordinates. Finally, doubling the cube and trisecting certain angles requires solving certain cubic equations that can be proved to have no rational roots. The Isabelle proofs require a great many detailed calculations.