John Harrison.
Proceedings of the 1993 International Workshop on the HOL theorem proving
system and its applications, Vancouver. Springer LNCS 780, pp. 426-436,
1993.

**NB! This paper is preliminary, and will be superseded by a chapter
of the author's forthcoming PhD thesis.**

## Abstract:

The elementary theory of real algebra, including multiplication, is decidable.
More precisely, there is an algorithm to eliminate quantifiers which does not
introduce new free variables or new constants other than rational numbers.
Therefore if a closed term of elementary real algebra involves no constants
other than the rational numbers, its truth or falsity can be determined
automatically. Quite a number of interesting algebraic and geometric problems
can be expressed in this decidable subset. In this paper we describe a HOL
implementation of a quantifier-elimination procedure and give some preliminary
results.
## Bibtex entry:

@INPROCEEDINGS{harrison-hol93,
crossref = "hol93",
author = "John Harrison",
title = "A {HOL} Decision Procedure for Elementary Real
Algebra",
pages = "426--436"}
@PROCEEDINGS{hol93,
editor = "Jeffrey J. Joyce and Carl Seger",
booktitle = "Proceedings of the 1993 International Workshop on
the {HOL} theorem proving system and its
applications",
series = "Lecture Notes in Computer Science",
volume = 780,
address = "UBC, Vancouver, Canada",
date = "August 1993",
year = 1993,
publisher = "Springer-Verlag"}