A case-study in algebraic manipulation using mechanized reasoning tools

References

• Andrés , M. , Lambán , L. and Rubio , J. Executing in common lisp, proving in ACL2 . Proceedings of Calculemus 2007 . Hagenberg, Austria. Edited by: Kauers , M. Vol. 4573 , pp. 1 – 12 . Berlin : Springer . Lecture Notes on Computer Science
   Google Scholar
• Aransay , J. , Ballarin , C. and Rubio , J. Towards a higher reasoning level in formalized Homological Algebra . Proceedings of Calculemus 2003 . Rome, Italy. Edited by: Hardin , T. and Rioboo , R. pp. 84 – 88 . Rome : Aracne Editrice S.R.L .
   Google Scholar
• Aransay , J. , Ballarin , C. and Rubio , J. Four approaches to automated reasoning with differential algebraic structures . Proceedings of the International Conference on Artificial Intelligence and Symbolic Computation, AISC 2004 . Linz, Austria. Edited by: Buchberger , B. and Campbell , J. A. Vol. 3249 , pp. 222 – 235 . Berlin : Springer . Lecture Notes in Artificial Intelligence
   Google Scholar
• Aransay , J. , Ballarin , C. and Rubio , J. 2008 . A mechanized proof of the basic perturbation lemma . J. Automat. Reason. , 40 : 271 – 292 .
   Google Scholar
• Bertot , Y. and Castéran , P. 2004 . “ Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions ” . Vol. 25 , Berlin, , Germany : Springer . Texts in Theoretical Computer Science
   Google Scholar
• Chaieb , A. and Wenzel , M. Context aware calculation and deduction–Ring equalities via Gröbner bases in Isabelle . Proceedings of Calculemus 2007 . Hagenberg, Austria. Edited by: Kauers , M. Vol. 4573 , pp. 27 – 39 . Berlin : Springer . Lecture Notes on Computer Science
   Google Scholar
• Church , A. 1940 . A formulation of the simple theory of types . J. Symbolic Logic , 5 : 56 – 68 .
   Google Scholar
• Coquand , T. and Huet , G. 1988 . The calculus of constructions . Inform. Comput. , 76 : 95 – 120 .
   Google Scholar
• Domínguez , C. Formalizing in Coq hidden algebras to specify symbolic computation systems . Proceedings of Calculemus 2008 . Birmingham, UK. Edited by: Autexier , S. Vol. 5144 , pp. 270 – 284 . Berlin : Springer . Lecture Notes on Computer Science
   Google Scholar
• Domínguez , C. , Lambán , L. and Rubio , J. 2007 . Object-oriented institutions to specify symbolic computation systems . Rairo Theor. Inf. Appl. , 41 : 191 – 214 .
   Google Scholar
• Domínguez , C. , Rubio , J. and Sergeraert , F. 2006 . Modeling inheritance as coercion in the Kenzo system . J. UCS , 12 : 1701 – 1730 .
   Google Scholar
• X. Dousson, F. Sergeraert, and Y. Siret, The Kenzo program, 1999. Available at http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/
   Google Scholar
• Eilenberg , S. and Zilber , J. 1953 . On products of complexes . Amer. J. Math. , 75 : 200 – 204 .
   Web of Science ®Google Scholar
• Kaufmann , M. , Manolios , P. and Strother-Moore , J. 2000 . “ Computer-Aided Reasoning: An Approach ” . Boston, , USA : Kluwer Academic Press .
   Google Scholar
• Lambán , L. , Pascual , V. and Rubio , J. 2003 . An object-oriented interpretation of the EAT system . Appl. Algebra Eng. Commun. Comput. , 14 : 187 – 215 .
   Google Scholar
• Mahboubi , A. Proving formally the implementation of an efficient gcd algorithm for polynomials . Proceedings of the International Joint Conference Automated Reasoning, IJCAR 2006 . Seattle, WA, USA. Edited by: Furbach , U. and Shankar , N. Vol. 4130 , pp. 438 – 452 . Berlin : Springer . Lecture Notes on Computer Science
   Google Scholar
• May , J. P. 1967 . Simplicial objects in Algebraic Topology Van Nostrand Mathematical Studies Vol. 11, D. Van Nostrand Co
   Google Scholar
• Müller , O. and Slind , K. 1997 . Treating partiality in a logic of total functions . Comput. J. , 40 : 640 – 652 .
   Google Scholar
• Newell , A. , Shaw , J. and Simon , H. Report on a general problem-solving program . Proceedings of the International Conference on Information Processing . pp. 256 – 264 . Paris : Unesco .
   Google Scholar
• Nipkow , T. , Paulson , L. C. and Wenzel , M. 2002 . “ Isabelle/HOL: A proof assistant for higher order logic ” . Vol. 2283 , Berlin, , Germany : Springer . Lecture Notes in Computer Science
   Google Scholar
• Paulin-Mohring , C. Inductive definitions in the system coq-rules and properties . Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA ’93 . Edited by: Bezem , M. and Groote , J. F. Vol. 664 , pp. 328 – 345 . Berlin : Springer . Lecture Notes on Computer Science
   Google Scholar
• Paulson , L. C. , Nipkow , T. and Wenzel , M. Isabelle Theory Library , Available at http://isabelle.in.tum.de/library/
   Google Scholar
• Rubio , J. and Sergeraert , F. 2002 . Constructive algebraic topology . Bull. Sci. Math. , 126 : 389 – 412 .
   Google Scholar
• Rubio , J. , Sergeraert , F. and Siret , Y. 1997 . “ EAT: Symbolic software for effective homology computation ” . Grenoble : Institut Fourier . Tech. Rep Available at ftp://ftp-fourier.ujf-grenoble.fr/pub/EAT
   Google Scholar
• Wiedijk , F. 2006 . The Seventeen Provers of the World, Foreword by Dana S. Scott , Edited by: Wiedijk , F. Vol. 3600 , Berlin, , Germany : Springer . Lecture Notes in Computer Science
   Google Scholar