Modelling algebraic structures and morphisms in ACL2

Autor: Heras Vicente, Jonathan; Martin-Mateos, F.J.; Pascual Martínez-Losa, María Vico

Tipo de documento: Artículo de revista

Revista: Applicable Algebra in Engineering, Communications and Computing. ISSN: 0938-1279. Año: 2015. Número: 3. Volumen: 26. Páginas: 277-303.

doi 10.1007/s00200-015-0252-9Texto completo open access 

SCIMAGO (datos correspondientes al año 2014):
SJR:
,457  SNIP: 1,126 

CIRC: GRUPO A

Referencias:

  • Adams, A., Computer algebra meets automated theorem proving: integrating Maple and PVS (2001) 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), Lecture Notes in Computer Science, vol. 2152, pp. 27-42
  • Andrés, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L., Formalizing simplicial topology in ACL2 (2007) 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007), pp. 34-39
  • Aransay, J., Ballarin, C., Rubio, J., A mechanized proof of the Basic Perturbation Lemma (2008) J. Autom. Reason., 40 (4), pp. 271-292
  • Aransay, J., Ballarin, C., Rubio, J., Generating certified code from formal proofs: a case study in homological algebra (2010) Formal Asp. Comput., 22 (2), pp. 193-213
  • 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)Armstrong, A., Struth, G., Weber, T., Programming and automating mathematics in the Tarski-Kleene hierarchy (2014) J. Log. Algebr. Methods Program., 83 (2), pp. 87-102
  • Bailey, A., (1999) The Machine-Checked Literate Formalisation of Algebra in Type Theory, , PhD thesis: Manchester University
  • Ballarin, C., Algebraic structures in Axiom and Isabelle: attempt at a comparison (2007) Programming Languages for Mechanized Mathematics (PLMMS 2007), number 07–10 in RISC-Linz Report Series, pp. 75-80
  • Ballarin, C., Aransay, J., Hohe, S., Kammller, F., Paulson (2013) L.: The Isabelle/HOL Algebra Library, , http://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf
  • Ballarin, C., Homann, K., Calmet, J., Theorems and algorithms: an interface between Isabelle and Maple (1995) 20th International Symposium on Symbolic and Algebraic Computation (ISSAC 1995). ACM Press, pp. 150-157
  • Bauer, A., Clarke, E.M., Zhao, X., Analytica—an experiment in combining theorem proving and symbolic computation (1998) J. Autom. Reason., 21 (3), pp. 295-325
  • Bishop, E.A., (1967) Foundations of Constructive Analysis, , McGraw-Hill, New York
  • Brock, B., (1997) Defstructure for ACL2 version 2.0, , www.cs.utexas.edu/users/moore/publications/others/defstructure-brock.ps, Technical report: Computational Logic Inc
  • Capretta, V., Universal algebra in type theory (1999) 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1999), Lecture Notes in Computer Science, vol. 1690, pp. 131-148
  • Castéran, P., Sozeau, M., (2014) A Gentle Introduction to Type Classes and Relations in Coq, , http://hal.inria.fr/hal-00702455, Technical report, INRIA
  • Chyzak, F., Mahboubi, A., Sibut-Pinote, T., Tassi, E., A computer-algebra-based formal proof of the irrationality of $$\zeta (3)$$ζ(3) (2014) 5th International Conference on Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science, vol. 8558, pp. 160-176
  • Denecke, K., Wismath, S.L., (2002) Universal Algebra and Applications in Theoretical Computer Science, , Chapman Hall/CRC, Boca Raton
  • Dénès, M., Mörtberg, A., Siles, V., A refinement-based approach to computational algebra in Coq (2012) 3rd International Conference on Interactive Theorem Proving (ITP 2012), Lecture Notes in Computer Science, vol. 7406, pp. 83-96
  • Domínguez, C., Rubio, J., Computing in Coq with infinite algebraic data structures (2010) 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2010), Lecture Notes in Artificial Intelligence, vol. 6167, pp. 204-218
  • Domínguez, C., Rubio, J., Effective Homology of Bicomplexes, formalized in Coq (2011) Theor. Comput. Sci., 412, pp. 962-970
  • Dousson, X., Rubio, J., Sergeraert, F., Siret, Y., (1998) The Kenzo program, , http://www-fourier.ujf-grenoble.fr/sergerar/Kenzo/, Institut Fourier, Grenoble
  • Durán, A.J., Pérez, M., Varona, J.L., The misfortunes of a mathematicians’ trio using computer algebra systems: can we trust? (2014) Not. Am. Math. Soc., 61 (10), pp. 1249-1252
  • Foster, S., Struth, G., Weber, T., Automated engineering of relational and algebraic methods in Isabelle/HOL—(Invited Tutorial) (2011) 12th International Conference Relational and Algebraic Methods in Computer Science (RAMICS 2011), pp. 52-67
  • Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L., Packaging mathematical structures (2009) 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Lecture Notes in Computer Science, vol. 5674, pp. 327-342
  • Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J., A constructive algebraic hierarchy in Coq (2002) J. Symb. Comput., 34 (4), pp. 271-286
  • Geuvers, H., Wiedijk, F., Zwanenburg, J., Pollack, R., Barendregt, H., The “Fundamental Theorem of Algebra” Project (2000) Technical report, , http://www.cs.kun.nl/gi/projects/fta
  • Gonthier, G., A machine-checked proof of the odd order theorem (2013) 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science, vol. 7998, pp. 163-179
  • Greve, D., Parameterized congruences in ACL2 (2006) 6th International Workshop on the ACL2 Theorem Prover and its Applications, pp. 28-34
  • Gunter, E., Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Department of Computer and Information Science, Moore School of Engineering (1989) University of Pennsylvania, , http://repository.upenn.edu/cis_reports/789/
  • Haftmann, F., (2014) Haskell-style type classes with Isabelle/Isar, , http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2014/doc/classes.pdf, Technical report, Technische Universität München
  • Harrison, J., Théry, L., A skeptic’s approach to combining HOL and Maple (1998) J. Autom. Reason., 21 (3), pp. 279-294
  • http://www.reduce-algebra.com/index.htm, Hearn, A.C., et al.: Reduce (2009)Heras, J., Mathematical Knowledge Management in Algebraic Topology, chapter An ACL2 infrastructure to formalize Kenzo Higher Order constructors, PhD thesis (2011) University of La Rioja, pp. 293-312. , http://www.unirioja.es/servicios/sp/tesis/22488.shtml
  • Heras, J., Martín-Mateos, F.J., Pascual, V., (2012) Implementing Algebraic Structures in ACL2, , http://www.unirioja.es/cu/joheras/ahomsia/, Technical report: University of La Rioja
  • Heras, J., Pascual, V., Rubio, J., A certified module to study digital images with the Kenzo system (2011) 13th International Conference on Computer Aided Systems Theory (EUROCAST 2011), Lecture Notes in Computer Science, vol. 6927, pp. 113-120
  • Heras, J., Pascual, V., Rubio, J., Proving with ACL2 the correctness of simplicial sets in the Kenzo system (2011) 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Lecture Notes in Computer Science, vol. 6564, pp. 37-51
  • Jackson, P., (1995) Enhancing the Nuprl Proof-Development System and Applying it to Computational Abstract Algebra, , PhD thesis: Cornell University
  • Jenks, R., Sutor, R., (1992) AXIOM: The Scientific Computation System, , Springer, Berlin
  • http://www.mizar.org/JFM/, Journal of Formalized Mathematics. 1990-presentKaliszyk, C., Wiedijk, F., Certified computer algebra on top of an interactive theorem prover (2007) 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2007), Lecture Notes in Computer Science, vol. 4108, pp. 94-105
  • Kaufmann, M., Manolios, P., Moore, J.S., (2000) Computer-Aided Reasoning: An Approach, , Kluwer, Dordrecht
  • Kaufmann, M., Moore, J.S., Structured theory development for a mechanized logic (2001) J. Autom. Reason., 26 (2), pp. 161-203
  • Kaufmann, M., Moore, J.S., (2014) ACL2 version, 6, p. 5. , http://www.cs.utexas.edu/users/moore/acl2/
  • Lambán, L., Martín-Mateos, F.J., Ruiz-Reina, J.L., Rubio, J., Formalization of a normalization theorem in simplicial topology (2012) Ann. Math. Artif. Intell., 64 (1), 37p
  • Lambán, L., Pascual, V., Rubio, J., Specifying implementations (1999) 24th International Symposium on Symbolic and Algebraic Computation (ISSAC 1999), ACM Press, pp. 245-251
  • Lambán, L., Pascual, V., Rubio, J., An object-oriented interpretation of the EAT system (2003) Appl. Algebra Eng. Commun. Comput., 14, pp. 187-215
  • 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 (2014) Log. J. IGPL, 22 (1), pp. 39-65
  • Manolios, P., Moore, J.S., Partial functions in ACL2 (2003) J. Autom. Reason., 31 (2), pp. 107-127
  • 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 (2002) 3rd International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2002), pp. 188-201
  • Martín-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L., ACL2 verification of simplicial degeneracy programs in the Kenzo system (2009) 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus 2009), of Lecture Notes in Computer Science, vol. 5625, pp. 106-121
  • Maunder, C.R.F., (1996) Algebraic Topology, , Dover, New York
  • http://maxima.sourceforge.net, Maxima, a Computer Algebra system (2012)Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.L., A verified Common Lisp implementation of Buchberger’s algorithm in ACL2 (2010) J. Symb. Comput., 45 (1), pp. 96-123
  • Naraschewski, W., Wenzel, M., Object-oriented verification based on record subtyping in higher-order logic (1998) 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1998), Lecture Notes in Computer Science, vol. 1479, pp. 349-366
  • Pessaux, F., Weia, P., Doligez, D., The FoCaLiZe essential (2010) Technical report, , http://focalize.inria.fr/
  • Pottier, L., (2001) User contributions in Coq, , http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4, Algebra, Technical report
  • Romero, A., Heras, J., Rubio, J., Sergeraert, F., Defining and computing persistent Z-homology in the general case (2014) CoRR, abs/1403, p. 7086
  • Romero, A., Rubio, J., Homotopy groups of suspended classifying spaces: an experimental approach (2013) Math. Comput., 82, pp. 2237-2244
  • Rubio, J., Sergeraert, F., (2006) Constructive Homological Algebra and Applications, , Algorithms, and Proofs. University of Genova, Lecture Notes Summer School on Mathematics
  • Rudnicki, P., Schwarzweller, C., Trybulec, A., Commutative Algebra in the Mizar System (2001) J. Symb. Comput., 32, pp. 143-169
  • Sergeraert, F., (1992) Effective Homology, a Survey, , http://www-fourier.ujf-grenoble.fr/sergerar/Papers/Survey.pdf, Technical report, Institut Fourier
  • Sergeraert, F., (2001) Common Lisp, Typing and Mathematics, , http://www-fourier.ujf-grenoble.fr/sergerar/Papers/Ezcaray.pdf, Technical report, Institut Fourier
  • Spitters, B., van der Weegen, E., Type classes for mathematics in type theory (2011) Math. Struct. Comput. Sci., 21, pp. 795-825
  • Weibel, C.A., (1994) An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics, , 38, Cambridge University Press, Cambridge
  • Yu, X., Hickey, J., (2003) Formalizing Abstract Algebra in Constructive Set Theory, , http://authors.library.caltech.edu/27065/, Technical report: California Institute of Technology
  • Zippel, R., The weyl computer algebra substrate (1993) International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO 1993), Lecture Notes in Computer Science, vol. 722, pp. 303-318