A case-study in algebraic manipulation using mechanized reasoning tools

DOI10.1080/00207160802676604MaRDI QIDQ5747731zbMATH OpenOpenAlexDBLPWikidataFDO

Authors

Publication date 14 September 2010

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

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

zbMATH Keywords

symbolic computationCoqIsabelle/HOLalgebraic manipulationmechanized reasoning tools

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Artificial Intelligence and Symbolic Computation
• A mechanized proof of the basic perturbation lemma
• A system for computing and reasoning in algebraic topology
• Modelling algebraic structures and morphisms in ACL2
• scientific article; zbMATH DE number 1222424

Cites work

• scientific article; zbMATH DE number 3181472 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 3264757 (Why is no real title available?)
• A formulation of the simple theory of types
• A mechanized proof of the basic perturbation lemma
• An object-oriented interpretation of the EAT system
• Artificial Intelligence and Symbolic Computation
• Constructive algebraic topology
• Context Aware Calculation and Deduction
• Executing in Common Lisp, Proving in ACL2
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Object oriented institutions to specify symbolic computation systems
• On Products of Complexes
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• The calculus of constructions
• The seventeen provers of the world. Foreword by Dana S. Scott..

Cited in

(1)

• Artificial Intelligence and Symbolic Computation

Describes a project that uses

Uses Software

• EAT
• Kenzo
• Isabelle/HOL
• Coq

This page was built for publication: A case-study in algebraic manipulation using mechanized reasoning tools

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