Skolem Functions and Herbrand Universes in a Tree Generalization of First Order Logic

Skolem functions and Herbrand universes are fundamental concepts in first-order logic that form the basis of many works in artificial intelligence. In this paper, we study a fragment of the XML Query Language (XQuery) that generalizes first-order logic to a setting where variables form a forest instead of a set. A formal description of the logic and its semantics is given; Skolem functions and Herbrand universes are generalized to this setting.