Commutative algebra in the Mizar system

DOI10.1006/jsco.2001.0456zbMath1074.68081OpenAlexW1968315351MaRDI QIDQ597122

Christoph Schwarzweller, Piotr Rudnicki, Andrzej Trybulec

Publication date: 6 August 2004

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/5cc9c1e64f96a858cb80e0578f395b538df0696f

zbMATH Keywords

Mizar Mathematical Library

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Computational aspects and applications of commutative rings (13P99)

Related Items (14)

Four decades of {\textsc{Mizar}}. Foreword ⋮ Packaging Mathematical Structures ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Computational logic: its origins and applications ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ On bag of 1. I ⋮ Introduction to algebraic geometry ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ On the Structure of Mizar Types ⋮ Point-Free, Set-Free Concrete Linear Algebra ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2 ⋮ Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking ⋮ A formalization of the Smith normal form in higher-order logic ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• AXIOM
• Theorema
• Mizar

Cites Work

• A machine-checked implementation of Buchberger's algorithm
• On equivalents of well-foundedness. An experiment in MIZAR
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Commutative algebra in the Mizar system