We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas (...) built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers. (shrink)

We consider the structure of all labeled trees, called also infinite terms, in the first order language with function symbols in a recursive signature of cardinality at least two and at least a symbol of arity two, with equality and a binary relation symbol which is interpreted to be the subtree relation. The existential theory over of this structure is decidable (see Tulipani [9]), but more complex fragments of the theory are undecidable. We prove that the theory of the structure (...) is in , where formulas are those in prenex form consisting of a string of unbounded existential quantifiers followed by a string of arbitrary quantifiers all bounded with respect to . Since the fragment of the theory was already known to be -hard (see Marongiu and Tulipani [5]), it is now established to be -complete. (shrink)

Given a prime p, we exhibit a Horn sentence H p which expresses "the cardinality is not p" and has size O(p 5 log p).