scientific article; zbMATH DE number 1389645

MaRDI QIDQ4934138zbMATH OpenFDO

Authors Clemens Ballarin, Lawrence C. Paulson

Publication date 17 January 2000

zbMATH Keywords

computer algebra

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Theory of error-correcting codes and error-detecting codes (94B99)

Recommendations

• scientific article; zbMATH DE number 1222424
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• scientific article; zbMATH DE number 1863375
• Integrating computer algebra into proof planning
• Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system

Cited in

(14)

• A library for formalization of linear error-correcting codes
• A reconstruction and extension of Maple's assume facility via constraint contextual rewriting
• A bi-directional extensible interface between Lean and Mathematica
• Interfacing computer algebra and deduction systems via the logic broker architecture
• A coding theoretic study of MLL proof nets
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• scientific article; zbMATH DE number 1222424 (Why is no real title available?)
• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 2000435 (Why is no real title available?)
• Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework
• Artificial Intelligence and Symbolic Computation
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Proving an execution of an algorithm correct?
• Formalising new mathematics in Isabelle: diagonal Ramsey

Describes a project that uses

Uses Software

• ALDOR
• AXIOM
• Isabelle

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4934138)