Title: On the Alternation-free Horn mu-calculus Authors: Jean-Marc Talbot Abstract: The Horn mu-calculus is a formalism extending logic programs by specifying for every predicate symbol with which (greatest or least) fix-point semantics, its denotation has to be computed. When applied to particular logic programs, called uniform, the Horn mu-calculus provides a syntactic extension for Rabin tree automata. However, it has been shown [Charatonik et al.:LICS98] that the denotation of the Horn mu-calculus applied to a uniform program remains a regular set of trees and that moreover, the emptiness of the denotation of a predicate p is a DEXPTIME-complete problem (in the size of the program). In [Charatonik_Niwinski_Podelski:Draft98], these results have been extended to uniform programs that may contain both existential and universal quantifications on the variables occurring in the body of ``clauses''. However, with this extension, the best known algorithm for testing the emptiness of the denotation of a predicate is doubly-exponential in the size of the program. In this paper, we consider those uniform logic programs with both kinds of quantification in the body. But we add to the Horn mu-calculus a limitation on the way the fix-point semantics is specified for predicates. This restriction is close to the one defining the alternation-free fragment of the mu-calculus. Therefore, we name this fragment of the Horn mu-calculus the alternation-free fragment. We devise for it an algorithm which performs the emptiness test for the denotation of a predicate in single-exponential time in the size of the program. To obtain this result, we develop a constructive approach based on a new kind of tree automata running on finite and infinite trees, called monotonous tree automata. These automata are defined by means of a family of finite and complete lattices. The acceptance condition for monotonous tree automata is based on the ordering relations of the lattices.