Modelling algebraic structures and morphisms in ACL2 (Q2349534): Difference between revisions

@@ Property / DOI @@
-.1007/s00200-015-0252-9
@@ Property / DOI: 10.1007/s00200-015-0252-9 / rank @@
-Normal rank
@@ Property / author @@
-Francisco Jesús Martín-Mateos
@@ Property / author: Francisco Jesús Martín-Mateos / rank @@
-Normal rank
@@ Property / author @@
+Francisco Jesús Martín-Mateos
@@ Property / author: Francisco Jesús Martín-Mateos / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Maxima
@@ Property / describes a project that uses: Maxima / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+EAT
@@ Property / describes a project that uses: EAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FoCaLiZe
@@ Property / describes a project that uses: FoCaLiZe / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AXIOM
@@ Property / describes a project that uses: AXIOM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Maple
@@ Property / describes a project that uses: Maple / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Analytica
@@ Property / describes a project that uses: Analytica / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Kenzo
@@ Property / describes a project that uses: Kenzo / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2053634551
@@ Property / OpenAlex ID: W2053634551 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790649
@@ Property / cites work: Q4790649 / rank @@
+Normal rank
@@ Property / cites work @@
+A Skeptic's approach to combining HOL and Maple
@@ Property / cites work: A Skeptic's approach to combining HOL and Maple / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanized proof of the basic perturbation lemma
+Normal rank
@@ Property / cites work @@
+Generating certified code from formal proofs: a case study in homological algebra
+Normal rank
@@ Property / cites work @@
+Formalization and Execution of Linear Algebra: From Theorems to Algorithms
+Normal rank
@@ Property / cites work @@
+Programming and automating mathematics in the Tarski-Kleene hierarchy
+Normal rank
@@ Property / cites work @@
+Effective homology of bicomplexes, formalized in Coq
+Normal rank
@@ Property / cites work @@
+Q4227289
@@ Property / cites work: Q4227289 / rank @@
+Normal rank
@@ Property / cites work @@
+Analytica --- an experiment in combining theorem proving and symbolic computation
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945205
@@ Property / cites work: Q4945205 / rank @@
+Normal rank
@@ Property / cites work @@
+A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
+Normal rank
@@ Property / cites work @@
+Q2784580
@@ Property / cites work: Q2784580 / rank @@
+Normal rank
@@ Property / cites work @@
+A Refinement-Based Approach to Computational Algebra in Coq
+Normal rank
@@ Property / cites work @@
+Computing in Coq with Infinite Algebraic Data Structures
+Normal rank
@@ Property / cites work @@
+The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
+Normal rank
@@ Property / cites work @@
+Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / rank @@
+Normal rank
@@ Property / cites work @@
+A constructive algebraic hierarchy in Coq.
@@ Property / cites work: A constructive algebraic hierarchy in Coq. / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Structured theory development for a mechanized logic
+Normal rank
@@ Property / cites work @@
+Modelling algebraic structures and morphisms in ACL2
+Normal rank
@@ Property / cites work @@
+Partial functions in ACL2
@@ Property / cites work: Partial functions in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
+Normal rank
@@ Property / cites work @@
+An object-oriented interpretation of the EAT system
+Normal rank
@@ Property / cites work @@
+Q4023355
@@ Property / cites work: Q4023355 / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Computer Algebra on Top of an Interactive Theorem Prover
+Normal rank
@@ Property / cites work @@
+Formalization of a normalization theorem in simplicial topology
+Normal rank
@@ Property / cites work @@
+ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
+Normal rank
@@ Property / cites work @@
+Q5605151
@@ Property / cites work: Q5605151 / rank @@
+Normal rank
@@ Property / cites work @@
+A verified common lisp implementation of Buchberger's algorithm in ACL2
+Normal rank
@@ Property / cites work @@
+Q4247084
@@ Property / cites work: Q4247084 / rank @@
+Normal rank
@@ Property / cites work @@
+Commutative algebra in the Mizar system
@@ Property / cites work: Commutative algebra in the Mizar system / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy groups of suspended classifying spaces: An experimental approach
+Normal rank
@@ Property / cites work @@
+Type classes for mathematics in type theory
@@ Property / cites work: Type classes for mathematics in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4296949
@@ Property / cites work: Q4296949 / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S00200-015-0252-9
@@ Property / DOI: 10.1007/S00200-015-0252-9 / rank @@
+Normal rank