In this paper¹, 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. © Springer-Verlag Berlin Heidelberg 2005.

Limet S., Pillot P.

733.pdf    Gửi cho bạn bè

Từ khóa : Computability and decidability; Logic programming; Mathematical transformations; Synchronization; Theorem proving; Logic program transformation; Pseudo-regular theory; Tree tuple languages; Problem solving