The goal of this project is to design decision and solving procedures for constraints over unranked terms and hedges and to incorporate them into the general framework of constraint logic programming.
Unranked terms are built using unranked function symbols. Such symbols do not have a fixed arity. That means, different occurrences of the same function symbol in terms may have different number of arguments.
Along with unranked function symbols, terms may contain first- and second-order variables. The first-order variables are term variables and hedge variables. The second-order variables are function and context variables. Substitutions map them to the corresponding structures: Term variables are mapped to single terms, hedge variables to hedges (finite sequences of terms and hedge variables), function variables to function symbols or variables, and context variables to contexts (terms with a single occurrence of a special constant, called the hole).
Unranked terms and hedges have gained popularity in recent years because of interesting applications: They naturally model XML data, program schemata, ambients, multithreaded recursive program configurations where the number of parallel processes is unbounded, variadic functions in various programming languages, etc. They appear also in the areas like rewriting, knowledge representation, program analysis and transformation, just to name a few. Hence, including them into the framework of constraint logic programming can lead to an interesting and useful extension.
Yes another distinctive feature of the language considered in the proposal is that definite and indefinite desc_ription operators,
Russell's iota and Bourbaki's tau (aka Hilbert`s epsilon) are permitted in terms.
Equational atom is an equation between terms. Membership atom requires possible values of a hedge or a context variable to belong respectively to a regular hedge or regular context language. Constraints are built from equational and membership atoms with the help of negation, disjunction, and conjunction.
Terms with desc_ription operators in constraints help to express a complex constraint compactly and, often, to avoid unnecessary computations.
The constraint language represented in this way is flexible and expressive, but it's expressive power should be restricted to make
computations feasible.
The project aims at finding such syntactic restrictions of constraints that are, on the one hand, expressive enough and, on the other hand, permit an efficient decision procedure. For such fragments, development of decision and solving algorithms, proving their properties (termination, soundness, completeness), and implementing them are planned.
Other line of research will be concerned with identifying syntactic restrictions on program clauses and goals to guarantee
generation of decidable and finitary constraints during inference.
Significance of the expected results of the project are twofold: First, they will extend the class of the existing formalisms of constraint solving by bringing in a new, expressive constraints and designing decision and solving techniques for them. Second, they will expand the application area of constraint logic programming to the domains whose modeling requires abstraction by unranked terms and hedges.

Project members:

• Temur Kutsia (Principal Investigator)

• Temur Jangveladze (Coordinator)

• Khimuri Rukhaia (Key Personnel)

• Lali Tibua (Key Personnel)

• Besik Dundua (Key Personnel)

• Gela Chankvetadze (Key Personnel)