Now showing items 1-3 of 3

    • A Decision Procedure for the First Order Theory of Real Addition with Order 

      Ferrante, Jeanne; Rackoff, Charles (1973-05)
      Consider the first order theory of the real numbers with the predicates + (plus) and < (less than). Let S be the set of true sentences. We first present an elimination of quantifiers decision procedure for S, and then ...
    • The Emptiness Problem for Automata on Infinite Trees 

      Hossley, Robert; Rackoff, Charles (1972-06)
      The purpose of this paper is to give an alternative proof to the decidability of the emptiness problem for tree automata, as shown in Rabin [4]. The proof reduces the emptiness problem for automata on infinite trees to ...
    • On the Complexity of the Theories of Weak Direct Products 

      Rackoff, Charles (1974-01)
      Let N be the set of nonnegative integers and let < N ,+> be the weak direct product of < N,+> with itself. Mostowski[ 9 ] shows that the theory of < N ,*> is decidable, but his decision procedure isn't elementary recursive. ...