Modelling algebraic structures and morphisms in ACL2

DOI10.1007/s00200-015-0252-9zbMath1325.68214OpenAlexW2053634551MaRDI QIDQ2349534

Vico Pascual, Jónathan Heras, Francisco Jesús Martín-Mateos

Publication date: 22 June 2015

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL: https://idus.us.es/handle//11441/86550

zbMATH Keywords

computer algebra systemsformal verificationACL2mathematical structuresalgebraic hierarchyproof engineering

Mathematics Subject Classification ID

Related Items (2)

Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• ACL2
• AXIOM
• Coq
• Isabelle
• Maple
• Maxima
• Isabelle/HOL
• Isabelle/Isar
• PVS
• Mizar
• Kenzo
• EAT
• Analytica
• FoCaLiZe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Commutative algebra in the Mizar system
• Effective homology of bicomplexes, formalized in Coq
• A mechanized proof of the basic perturbation lemma
• Generating certified code from formal proofs: a case study in homological algebra
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• A Skeptic's approach to combining HOL and Maple
• Analytica --- an experiment in combining theorem proving and symbolic computation
• A constructive algebraic hierarchy in Coq.
• An object-oriented interpretation of the EAT system
• Partial functions in ACL2
• Structured theory development for a mechanized logic
• Formalization of a normalization theorem in simplicial topology
• Modelling algebraic structures and morphisms in ACL2
• The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• A Refinement-Based Approach to Computational Algebra in Coq
• Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Type classes for mathematics in type theory
• Packaging Mathematical Structures
• Formalization and Execution of Linear Algebra: From Theorems to Algorithms
• Computing in Coq with Infinite Algebraic Data Structures
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
• Homotopy groups of suspended classifying spaces: An experimental approach
• A Machine-Checked Proof of the Odd Order Theorem
• Certified Computer Algebra on Top of an Interactive Theorem Prover

This page was built for publication: Modelling algebraic structures and morphisms in ACL2