Reseña: “Certified symbolic manipulation: Bivariate simplicial polynomials”

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en ACL2 titulado Certified symbolic manipulation: Bivariate simplicial polynomials.

Sus autores son Laureano Lambán, Francisco Jesús Martín Mateos, Julio Rubio y José Luis Ruiz Reina.

El trabajo se presentará en el ISSAC 2013 (38th International Symposium on Symbolic and Algebraic Computation).

Su resumen es

Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In this paper, we focus on algebraic algorithms implemented in the proof assistant ACL2, which allows us to verify correctness in the same programming environment. The case study is that of bivariate simplicial polynomials, a data structure used to help the proof of properties in Simplicial Topology. Simplicial polynomials can be computationally interpreted in two ways. As symbolic expressions, they can be handled algorithmically, increasing the automation in ACL2 proofs. As representations of functional operators, they help proving properties of categorical morphisms. As an application of this second view, we present the definition in ACL2 of some morphisms involved in the Eilenberg-Zilber reduction, a central part of the Kenzo computer algebra system. We have proved the ACL2 implementations are correct and tested that they get the same results as Kenzo does.

El código ACL2 de la formalización del teorema de Eilenberg-Zilber se encuentra aquí.

Reseña: Mechanical verification of SAT refutations with extended resolution

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en ACL2 titulado Mechanical verification of SAT refutations with extended resolution.

Sus autores son Nathan Wetzler, Marijn J. H. Heule y Warren A. Hunt Jr.

El trabajo se presentará en julio en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We present a mechanically-verified proof checker developed with the ACL2 theorem-proving system that is general enough to support the growing variety of increasingly complex satisfiability (SAT) solver techniques, including those based on extended resolution. A common approach to assure the correctness of SAT solvers is to emit a proof of unsatisfiability when no solution is reported to exist. Contemporary proof checkers only check logical equivalence using resolution-style inference. However, some state-of-the-art, conflict-driven, clause-learning SAT solvers use preprocessing, inprocessing, and learning techniques, that cannot be checked solely by resolution-style inference. We have developed a mechanically-verified proof checker that assures refutation clauses preserve satisfiability. We believe our approach is sufficiently expressive to validate all known SAT-solver techniques.

Reseña: Verifying refutations with extended resolution

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con ACL2 sobre sistemas SAT titulado Verifying refutations with extended resolution.

Sus autores son Marijn J. H. Heule, Warren A. Hunt, Jr. y Nathan Wetzler (de la Universidad de Tejas en Austin).

El trabajo se presentó la semana pasada en el CADE-24 (the 24th International Conference on Automated Deduction).

Su resumen es

Modern SAT solvers use preprocessing and inprocessing techniques that are not solely based on resolution; existing unsatisfiability proof formats do not support SAT solvers using such techniques. We present a new proof format for checking unsatisfiability proofs produced by SAT solvers that use techniques such as extended resolution and blocked clause addition. Our new format was designed with three goals: proofs should be easy to generate, proofs should be compact, and validating proofs must be simple. We show how existing preprocessors and solvers can be modified to generate proofs in our new format. Additionally, we implemented a mechanically-verified proof checker in ACL2 and a proof checker in C for the proposed format.

El correspondiente código ACL2 se encuentra aquí.

Reseña: A macro for reusing abstract functions and theorems

PorJosé A. Alonso

Se ha publicado un artículo sobre automatización del razonamiento en ACL2 titulado A macro for reusing abstract functions and theorems.

Sus autores son Sebastiaan J.C. Joosten, Bernard van Gastel y Julien Schmaltz (Open University of the Netherlands).

El trabajo se presentará en el ACL2 Workshop 2013 (Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications).

Su resumen es

Even though the ACL2 logic is first order, the ACL2 system offers several mechanisms providing users with some operations akin to higher order logic ones. In this paper, we propose a macro, named instance-of-defspec, to ease the reuse of abstract functions and facts proven about them. Defspec is an ACL2 book allowing users to define constrained functions and their associated properties. It contains macros facilitating the definition of such abstract specifications and instances thereof. Currently, lemmas and theorems derived from these abstract functions are not automatically instantiated. This is exactly the purpose of our new macro. instance-of-defspec will not only instantiate functions and theorems within a specification but also many more functions and theorems built on top of the specification. As a working example, we describe various fold functions over monoids, which we gradually built from arbitrary functions.

La macro instance-of-defspec es análoga a la presentada por F.J. Martín Mateos en el artículo A generic instantiation tool and a case study: a generic multiset theory, presentado en el ACL2 Workshop 2002, y cuyo resumen es

In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the theory be as independent of a concrete implementation as possible. This is particularly interesting when we design theories about basic data types, making those developments more general, reusable and extensible. At the same time, it would also be desirable to be able to instantiate (in a convenient way) the definitions and theorems of the theory, for a concrete implementation. In this paper we present the development of a particular generic theory, and a tool to instantiate its events. As a case study we have chosen to describe a generic theory about finite multisets. It is also shown how this generic theory can be instantiated (using several macros we have defined) to build a theory about two different implementations of multisets. Finally we propose some directions for further research in this topic.

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.