Reseña: One logic to use them all

PorJosé A. Alonso

Una de las principales barreras en el avance de la automatización del razonamiento consiste en la comunicación entre distintos sistemas de razonamiento. Una forma de superarla es la planteada en el artículo One logic to use them all.

Su autor es Jean-Christophe Filliâtre (de la Universidad de París-Sur).

El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).

Su resumen es

Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verification of many non-trivial programs.

Reseña: A fully verified executable LTL model checker

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado A fully verified executable LTL model checker.

Sus autores son Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf y Jan-Georg Smaus.

El trabajo se presentará en el CAV 2013 (25th International Conference on Computer Aided Verification).

Su resumen es

We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using recent Isabelle technology called the Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of “formalized pseudocode”, and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested. We report on the structure of the checker, the development process, and some experiments on standard benchmarks.

El trabajo forma parte del proyecto CAVA (Computer Aided Verification of Automata).

El código de las correspondientes teorías Isabelle/HOL se encuentra aquí.

Reseña: ForMaRE – formal mathematical reasoning in economics

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado a la economía titulado ForMaRE – formal mathematical reasoning in economics.

Sus autores son Manfred Kerber, Christoph Lange y Colin Rowat (de la Universidad de Birmingham) y lo presentarán hoy en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

We present the ForMaRE project which applies FORmal MAthematical REasoning to economics. Theoretical economics makes use of mathematical proof and we seek to increase confidence in these theoretical results by applying formal mathematical reasoning. This will lead on the one hand to new challenge problems in formal reasoning. On the other hand we are conducting research that connects economics and formal methods. We will discuss some areas of interest such as game theory and auctions, where we are currently building a toolbox of formalizations.

Reseña: AI over large formal knowledge bases: The first decade

PorJosé A. Alonso

Se ha publicado un artículo sobre aplicaciones de la inteligencia artificial a la demostración automática de teoremas titulado AI over large formal knowledge bases: The first decade.

Su autor es Josef Urban (de la Univ. de Nimega, Países Bajos) y lo presentará mañana en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

In March 2003, the first version of the Mizar Problems for Theorem Proving (MpTP) was released. In the past ten years, such large formal knowledge bases have started to provide an interesting playground for combining deductive and inductive AI methods. The talk will discuss three related areas of application in which machine learning and general AI have been recently experimented with: (i) premise selection for theorem proving over large formal libraries built with systems like Mizar, HOL Light, and Isabelle (ii) advising and tuning first-order automated theorem provers such as E and leanCoP, and (iii) building larger inductive/deductive AI systems such as MaLARea. Here I focus on the wider motivation for this work.

Reseña: Formalization of real analysis: A survey of proof assistants and libraries

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.

Su resumen es

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.