A case-study in algebraic manipulation using mechanized reasoning tools
From MaRDI portal
Publication:5747731
DOI10.1080/00207160802676604zbMath1205.68358OpenAlexW2051578513WikidataQ57721919 ScholiaQ57721919MaRDI QIDQ5747731
No author found.
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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The seventeen provers of the world. Foreword by Dana S. Scott..
- A mechanized proof of the basic perturbation lemma
- The calculus of constructions
- An object-oriented interpretation of the EAT system
- Isabelle/HOL. A proof assistant for higher-order logic
- Constructive algebraic topology
- Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
- Executing in Common Lisp, Proving in ACL2
- Context Aware Calculation and Deduction
- Object oriented institutions to specify symbolic computation systems
- Artificial Intelligence and Symbolic Computation
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- A formulation of the simple theory of types
- On Products of Complexes
This page was built for publication: A case-study in algebraic manipulation using mechanized reasoning tools
