Proving Equalities in a Commutative Ring Done Right in Coq
Authors:
- 1 January 2005
- book chapter
- Published by Springer Nature
- p. 98-113
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- A Decision Procedure for Geometry in CoqLecture Notes in Computer Science, 2004
- Interactive Theorem Proving and Program Development2004
- Setoids in type theoryJournal of Functional Programming, 2003
- A Tactic Language for the System Coq2002
- A Skeptic's Approach to Combining HOL and MapleJournal of Automated Reasoning, 1998
- Using reflection to build efficient and certified decision procedures1997
- A simple model for quotient types1995
- Quantifier elimination for real closed fields by cylindrical algebraic decompostion1975