Reseña: A macro for reusing abstract functions and theorems
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.