Solving First Order Formulae of Pseudo-Regular Theory.

In this paperA full version can be found in the LIFO RR-2005-2 at the following URL http://www.univ-orleans.fr/lifo/prodsci/rapports/RR2005.htm.en, we study the class of pseudo-regular relations which is an extension of regular relations that weakens some restrictions on the "synchronization" between tuple components of the relation. We choose logic programming as formalism to describe tree tuple languages (i.e. relations) and logic program transformation techniques for computing operations on them. We show that even if pseudo-regular cs-programs are syntactically less restrictive than regular ones, they define the same class of tree tuple languages. However, pseudo-regular relations allow one to define classes of term rewrite systems the transitive closure of which is a regular relation. We apply this result to give a decidable class of first order formulae based on the joinability predicate ↓?R where R is a pseudo-regular term rewrite system. [ABSTRACT FROM AUTHOR]