Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking

DOI10.1080/00207160701864459zbMath1178.68692OpenAlexW2022218102MaRDI QIDQ5852118

Adam Naumowicz

Publication date: 26 January 2010

Published in: International Journal of Computer Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/00207160701864459

zbMATH Keywords

Gröbner basesMIZARintegrating automated deduction and computer algebra

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Four decades of {\textsc{Mizar}}. Foreword, Mechanizing complemented lattices within Mizar type system, Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization, Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver, Improving legibility of formal proofs based on the close reference principle is NP-hard, Mizar: State-of-the-art and Beyond, The role of the Mizar mathematical library for interactive proof development in Mizar, Flexary connectives in Mizar, Accessing the Mizar Library with a Weakly Strict Mizar Parser, SAT-Enhanced Mizar Proof Checking

Uses Software

• CoCoA
• CoCoALib
• GAP
• Macaulay2
• SINGULAR
• Mizar

Cites Work

• Unnamed Item
• Commutative algebra in the Mizar system
• On the application of Buchberger's algorithm to automated geometry theorem proving
• A refutational approach to geometry theorem proving
• On equivalents of well-foundedness. An experiment in MIZAR
• Links to Projects. Mathematical Software, icms2006—Developer’s Meeting