Loading...
Please wait, while we are loading the content...
Similar Documents
An ACL2 formalization of algebraic structures
| Content Provider | Semantic Scholar |
|---|---|
| Author | Vicente, Jónathan Heras Martínez-Losa, María Vico Pascual |
| Copyright Year | 2012 |
| Abstract | In this paper we present a hierarchy of algebraic structures developed in the ACL2 Theorem Prover. This question had not been undertaken in this system up to now. A methodology and a bunch of tools to handle the structures and morphisms included in our hierarchy have been designed. In order to ensure the applicability of our methodology and tools, a major issue when developing formal proofs, we have proved some results coming from Universal Algebra. Introduction Proof Assistant tools are nowadays mature enough to tackle non-trivial mathematical problems; we can cite, among others, the formalizations of the Four Color Theorem [5], the Fundamental Theorem of algebra [4] or the Kepler conjecture [13]. The choice of a convenient representation for algebraic structures has been a cornerstone of all these projects. As a result of that, several algebraic hierarchies have been developed in Proof Assistant tools like Coq, Isabelle or Hol. However, as far as we know, this question had not been undertaken in ACL2 [10], a theorem prover designed to verify properties of code written in the programming language Common Lisp [6]. In this paper we present an ACL2 algebraic hierarchy which allows one to create theories about usual mathematical structures (the hierarchy ranges from setoids to R-modules including structures such as groups or rings) and morphisms between those structures. This ACL2 hierarchy is not only an end, but also a means to achieve our nal goal of verifying actual code of the Kenzo Computer Algebra system [3]. To test the suitability of our framework, we present how to use it to prove a result from Universal Algebra. 1. An algebraic hierarchy in ACL2 The hierarchy of mathematical structures and morphisms depicted in Figure 1 has been developed in ACL2, a preliminary approach was presented in [7]. In the left side of Figure 1, there are the mathematical structures of our hierarchy, ranging from setoids to R-modules. A detailed description of each one of these structures can be seen in [2]. A continuous arrow with an open triangle represents an inheritance relationship modeling that the source mathematical structure is-a target mathematical structure. Whereas a continuous arrow with a normal tip describes a use relationship in the sense that the target mathematical structure is used to de ne the source one. The morphisms included in our hierarchy are presented in the right side of Figure 1. It is worth noting that a morphism always consists of a source structure, A of type T , a target Partially supported by Ministerio de Educación y Ciencia, project MTM2009-13842-C02-01, and by the European Union's 7th Framework Programme under grant agreement nr. 243847 (ForMath). 1 2 JÓNATHAN HERAS, FRANCISCO-JESÚS MARTÍN-MATEOS, AND VICO PASCUAL |
| Starting Page | 103 |
| Ending Page | 106 |
| Page Count | 4 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www3.uah.es/eaca2012/textos/ponentes/heras_martin.pdf |
| Alternate Webpage(s) | https://www.unirioja.es/cu/joheras/papers/aafoas.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
