Extending the HOL theorem prover with a computer algebra system to reason about the reals

This publication has 12 references indexed in Scilit:

• Integrating A First-order Automatic prover In The HOL Environment
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
• Constructing the real numbers in HOL
  Published by Elsevier ,1993
• A Lazy Approach to Fully-Expansive Theorem Proving
  Published by Elsevier ,1993
• First Leaves: A Tutorial Introduction to Maple V
  Published by Springer Nature ,1992
• CAS/PI
  Published by Association for Computing Machinery (ACM) ,1992
• A two-level formal verification methodology using HOL and COSMOS
  Published by Springer Nature ,1992
• axịom™
  Published by Springer Nature ,1992
• A Unified Theory of Integration
  The American Mathematical Monthly, 1973
• Sets and integration An outline of the development
  Published by Springer Nature ,1972
• A Riemann-Type Integral of Lebesgue Power
  Canadian Journal of Mathematics, 1968