This paper provides the theoretical formalism for the automated deduction system developed by Bledsoe and Hines [1] which uses a variation of resolution to discover proofs about dense total orders without endpoints. In particular, the real numbers with their usual ordering is a dense total order without endpoints. As such, this system has been used to prove theorems about elementary calculus. Instead of adding the necessary order axioms directly to the system, they are incorporated through the inference rules of chaining, self-chaining, and factoring. The appropriate analog of Herbrand’s theorem and a ground resolution theorem are given. Furthermore, several completeness results are carefully proven for more restrictive forms of chaining. Lastly, an example which illustrates many of the ideas of the paper is presented, and results are compared with those actually obtained using the Bledsoe-Hines system.