×

Modelling algebraic structures and morphisms in ACL2. (English) Zbl 1325.68214

Summary: In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we illustrate a methodology for implementing a set of tools that facilitates the formalisations related to algebraic structures – as a result, an algebraic hierarchy ranging from setoids to vector spaces has been developed. The resultant tools can be used to simplify the development of generic theories about algebraic structures. In particular, the benefits of using the tools presented in this paper, compared to a from-scratch approach, are especially relevant when working with complex mathematical structures; for example, the structures employed in Algebraic Topology. This work shows that ACL2 can be a suitable tool for formalising algebraic concepts coming, for instance, from computer algebra systems.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Adams, A., et al.: Computer algebra meets automated theorem proving: integrating Maple and PVS. In: 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), Lecture Notes in Computer Science, vol. 2152, pp. 27-42 (2001) · Zbl 1005.68997
[2] Andrés, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing simplicial topology in ACL2. In: 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007), pp. 34-39 (2007) · Zbl 0916.68142
[3] Aransay, J., Ballarin, C., Rubio, J.: A mechanized proof of the Basic Perturbation Lemma. J. Autom. Reason. 40(4), 271-292 (2008) · Zbl 1140.68059 · doi:10.1007/s10817-007-9094-x
[4] Aransay, J., Ballarin, C., Rubio, J.: Generating certified code from formal proofs: a case study in homological algebra. Formal Asp. Comput. 22(2), 193-213 (2010) · Zbl 1214.68330 · doi:10.1007/s00165-009-0120-0
[5] Aransay, J., Divasón, J.: Formalization and execution of linear algebra: from theorems to algorithms. In: 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Lecture Notes in Computer Science (2013) (in press) · Zbl 1453.68210
[6] Armstrong, A., Struth, G., Weber, T.: Programming and automating mathematics in the Tarski-Kleene hierarchy. J. Log. Algebr. Methods Program. 83(2), 87-102 (2014) · Zbl 1434.68637 · doi:10.1016/j.jlap.2014.02.001
[7] Bailey, A.: The Machine-Checked Literate Formalisation of Algebra in Type Theory. PhD thesis, Manchester University (1999)
[8] Ballarin, C.: Algebraic structures in Axiom and Isabelle: attempt at a comparison. In: Programming Languages for Mechanized Mathematics (PLMMS 2007), number 07-10 in RISC-Linz Report Series, pp. 75-80 (2007)
[9] Ballarin, C., Aransay, J., Hohe, S., Kammller, F., Paulson, L.: The Isabelle/HOL Algebra Library (2013). http://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf · Zbl 1207.68211
[10] Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between Isabelle and Maple. In: 20th International Symposium on Symbolic and Algebraic Computation (ISSAC 1995). ACM Press, pp. 150-157 (1995) · Zbl 0922.68080
[11] Bauer, A., Clarke, E.M., Zhao, X.: Analytica—an experiment in combining theorem proving and symbolic computation. J. Autom. Reason. 21(3), 295-325 (1998) · Zbl 0916.68143 · doi:10.1023/A:1006079212546
[12] Bishop, E.A.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967) · Zbl 0183.01503
[13] Brock, B.: Defstructure for ACL2 version 2.0. Technical report, Computational Logic Inc (1997). www.cs.utexas.edu/users/moore/publications/others/defstructure-brock.ps
[14] Capretta, V.: Universal algebra in type theory. In: 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1999), Lecture Notes in Computer Science, vol. 1690, pp. 131-148 (1999) · Zbl 0947.08001
[15] Castéran, P., Sozeau, M.: A Gentle Introduction to Type Classes and Relations in Coq. Technical report, INRIA (2014). http://hal.inria.fr/hal-00702455
[16] Chyzak, F., Mahboubi, A., Sibut-Pinote, T., Tassi, E.: A computer-algebra-based formal proof of the irrationality of \[\zeta (3)\] ζ(3). In: 5th International Conference on Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science, vol. 8558, pp. 160-176 (2014) · Zbl 1416.68155
[17] Denecke, K., Wismath, S.L.: Universal Algebra and Applications in Theoretical Computer Science. Chapman Hall/CRC, Boca Raton (2002) · Zbl 0993.08001
[18] Dénès, M., Mörtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: 3rd International Conference on Interactive Theorem Proving (ITP 2012), Lecture Notes in Computer Science, vol. 7406, pp. 83-96 (2012) · Zbl 1360.68745
[19] Domínguez, C., Rubio, J.: Computing in Coq with infinite algebraic data structures. In: 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2010), Lecture Notes in Artificial Intelligence, vol. 6167, pp. 204-218 (2010) · Zbl 1286.68396
[20] Domínguez, C., Rubio, J.: Effective Homology of Bicomplexes, formalized in Coq. Theor. Comput. Sci. 412, 962-970 (2011) · Zbl 1207.68211 · doi:10.1016/j.tcs.2010.11.016
[21] Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo program. Institut Fourier, Grenoble (1998). http://www-fourier.ujf-grenoble.fr/sergerar/Kenzo/
[22] Durán, A.J., Pérez, M., Varona, J.L.: The misfortunes of a mathematicians’ trio using computer algebra systems: can we trust? Not. Am. Math. Soc. 61(10), 1249-1252 (2014) · Zbl 1338.68299 · doi:10.1090/noti1173
[23] Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle/HOL—(Invited Tutorial). In: 12th International Conference Relational and Algebraic Methods in Computer Science (RAMICS 2011), pp. 52-67 (2011) · Zbl 1329.68230
[24] Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Lecture Notes in Computer Science, vol. 5674, pp. 327-342 (2009) · Zbl 1252.68253
[25] Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271-286 (2002) · Zbl 1038.68108 · doi:10.1006/jsco.2002.0552
[26] Geuvers, H., Wiedijk, F., Zwanenburg, J., Pollack, R., Barendregt, H.: The “Fundamental Theorem of Algebra” Project. Technical report (2000). http://www.cs.kun.nl/gi/projects/fta · Zbl 1305.68157
[27] Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science, vol. 7998, pp. 163-179 (2013) · Zbl 1317.68211
[28] Greve, D.: Parameterized congruences in ACL2. In: 6th International Workshop on the ACL2 Theorem Prover and its Applications, pp. 28-34 (2006) · Zbl 0971.03017
[29] Gunter, E.: Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Department of Computer and Information Science, Moore School of Engineering, University of Pennsylvania (1989). http://repository.upenn.edu/cis_reports/789/
[30] Haftmann, F.: Haskell-style type classes with Isabelle/Isar. Technical report, Technische Universität München (2014). http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2014/doc/classes.pdf · Zbl 1214.68330
[31] Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. J. Autom. Reason. 21(3), 279-294 (1998) · Zbl 0916.68142 · doi:10.1023/A:1006023127567
[32] Hearn, A.C., et al.: Reduce (2009). http://www.reduce-algebra.com/index.htm · Zbl 0916.68142
[33] Heras, J.: Mathematical Knowledge Management in Algebraic Topology, chapter An ACL2 infrastructure to formalize Kenzo Higher Order constructors, PhD thesis, University of La Rioja, pp. 293-312 (2011). http://www.unirioja.es/servicios/sp/tesis/22488.shtml · Zbl 0916.68143
[34] Heras, J., Martín-Mateos, F.J., Pascual, V.: Implementing Algebraic Structures in ACL2. Technical report, University of La Rioja (2012). http://www.unirioja.es/cu/joheras/ahomsia/ · Zbl 1325.68214
[35] Heras, J., Pascual, V., Rubio, J.: A certified module to study digital images with the Kenzo system. In: 13th International Conference on Computer Aided Systems Theory (EUROCAST 2011), Lecture Notes in Computer Science, vol. 6927, pp. 113-120 (2011) · Zbl 1060.68109
[36] Heras, J., Pascual, V., Rubio, J.: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. In: 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Lecture Notes in Computer Science, vol. 6564, pp. 37-51 (2011) · Zbl 1326.68261
[37] Jackson, P.: Enhancing the Nuprl Proof-Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University (1995) · Zbl 1046.68140
[38] Jenks, R., Sutor, R.: AXIOM: The Scientific Computation System. Springer, Berlin (1992) · Zbl 0758.68010
[39] Journal of Formalized Mathematics. 1990-present. http://www.mizar.org/JFM/
[40] Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2007), Lecture Notes in Computer Science, vol. 4108, pp. 94-105 (2007) · Zbl 1202.68382
[41] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)
[42] Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161-203 (2001) · Zbl 0971.03017 · doi:10.1023/A:1026517200045
[43] Kaufmann, M., Moore, J.S.: ACL2 version 6.5 (2014). http://www.cs.utexas.edu/users/moore/acl2/ · Zbl 1038.68108
[44] Lambán, L., Martín-Mateos, F.J., Ruiz-Reina, J.L., Rubio, J.: Formalization of a normalization theorem in simplicial topology. Ann. Math. Artif. Intell. 64(1), 1-37 (2012) · Zbl 1280.68232 · doi:10.1007/s10472-011-9274-6
[45] Lambán, L., Pascual, V., Rubio, J.: Specifying implementations. In: 24th International Symposium on Symbolic and Algebraic Computation (ISSAC 1999), ACM Press, pp. 245-251 (1999)
[46] Lambán, L., Pascual, V., Rubio, J.: An object-oriented interpretation of the EAT system. Appl. Algebra Eng. Commun. Comput. 14, 187-215 (2003) · Zbl 1046.68140 · doi:10.1007/s00200-003-0129-1
[47] Lambán, L., Rubio, J., Martín-Mateos, F.J., Ruiz-Reina, J.L.: Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Log. J. IGPL 22(1), 39-65 (2014) · Zbl 1305.68157 · doi:10.1093/jigpal/jzt034
[48] Manolios, P., Moore, J.S.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107-127 (2003) · Zbl 1060.68109 · doi:10.1023/B:JARS.0000009505.07087.34
[49] Martín-Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz-Reina, J.L.: A generic instantiation tool and a case study: a generic multiset theory. In: 3rd International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2002), pp. 188-201 (2002)
[50] Martín-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: ACL2 verification of simplicial degeneracy programs in the Kenzo system. In: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2009), of Lecture Notes in Computer Science, vol. 5625, pp. 106-121 (2009) · Zbl 1247.68325
[51] Maunder, C.R.F.: Algebraic Topology. Dover, New York (1996) · Zbl 0205.27302
[52] Maxima, a Computer Algebra system (2012). http://maxima.sourceforge.net · Zbl 1338.68299
[53] Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.L.: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2. J. Symb. Comput. 45(1), 96-123 (2010) · Zbl 1194.68155 · doi:10.1016/j.jsc.2009.07.002
[54] Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1998), Lecture Notes in Computer Science, vol. 1479, pp. 349-366 (1998) · Zbl 0927.03026
[55] Pessaux, F., Weia, P., Doligez, D.: The FoCaLiZe essential. Technical report (2010). http://focalize.inria.fr/
[56] Pottier, L.: User contributions in Coq, Algebra. Technical report (2001). http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4 · Zbl 1074.68081
[57] Romero, A., Heras, J., Rubio, J., Sergeraert, F.: Defining and computing persistent Z-homology in the general case. CoRR, abs/1403.7086 (2014)
[58] Romero, A., Rubio, J.: Homotopy groups of suspended classifying spaces: an experimental approach. Math. Comput. 82, 2237-2244 (2013) · Zbl 1284.68684 · doi:10.1090/S0025-5718-2013-02680-4
[59] Rubio, J., Sergeraert, F.: Constructive Homological Algebra and Applications. Algorithms, and Proofs. University of Genova, Lecture Notes Summer School on Mathematics (2006)
[60] Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative Algebra in the Mizar System. J. Symb. Comput. 32, 143-169 (2001) · Zbl 1074.68081 · doi:10.1006/jsco.2001.0456
[61] Sergeraert, F.: Effective Homology, a Survey. Technical report, Institut Fourier (1992). http://www-fourier.ujf-grenoble.fr/sergerar/Papers/Survey.pdf · Zbl 1194.68155
[62] Sergeraert, F.: Common Lisp, Typing and Mathematics. Technical report, Institut Fourier (2001). http://www-fourier.ujf-grenoble.fr/sergerar/Papers/Ezcaray.pdf
[63] Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21, 795-825 (2011) · Zbl 1223.68105 · doi:10.1017/S0960129511000119
[64] Weibel, C.A.: An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics, vol. 38. Cambridge University Press, Cambridge (1994) · Zbl 0797.18001 · doi:10.1017/CBO9781139644136
[65] Yu, X., Hickey, J.: Formalizing Abstract Algebra in Constructive Set Theory. Technical report, California Institute of Technology (2003). http://authors.library.caltech.edu/27065/
[66] Zippel, R.: The weyl computer algebra substrate. In: International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO 1993), Lecture Notes in Computer Science, vol. 722, pp. 303-318 (1993)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.