A Proof-Producing Decision Procedure for Real Arithmetic
Authors:
- 1 January 2005
- book chapter
- Published by Springer Nature
- p. 295-314
Abstract
No abstract availableKeywords
This publication has 14 references indexed in Scilit:
- Integrating A First-order Automatic prover In The HOL Environment2005
- CVC Lite: A New Implementation of the Cooperating Validity Checker2004
- Linear and Nonlinear Arithmetic in ACL2Lecture Notes in Computer Science, 2003
- Some Points of Analysis and Their History1997
- Quantifier Elimination for Real Algebra -- the Quadratic Case and BeyondApplicable Algebra in Engineering, Communication and Computing, 1997
- Proof-carrying code1997
- HOL Light: A tutorial introduction1996
- Edinburgh LCF1979
- Decision procedures for real and p‐adic fieldsCommunications on Pure and Applied Mathematics, 1969
- A New Decision Method for Elementary AlgebraAnnals of Mathematics, 1954