Solving First Order Formulae of Pseudo-Regular Theory

  • Sébastien Limet
  • Pierre Pillot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


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 \(\downarrow^{\rm ?}_{R}\) where R is a pseudo-regular term rewrite system.


Logic Program Function Symbol Predicate Symbol Horn Clause Ground Atom 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)Google Scholar
  2. 2.
    Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (TATA) (1997),
  3. 3.
    Comon, H., Haberstrau, M., Jouannaud, J.-P.: Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation 111(1), 154–191 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Faßbender, H., Maneth, S.: A strict border for the decidability of e-unification for recursive functions. Journal of Functional and Logic Programming 1998(4) (1998)Google Scholar
  5. 5.
    Limet, S., Réty, P.: E-unification by means of tree tuple synchronized grammars. Discrete Mathematics and Theoretical Computer Science 1, 69–98 (1997)zbMATHMathSciNetGoogle Scholar
  6. 6.
    Limet, S., Salzer, G.: Manipulating tree tuple languages by transforming logic programs. Technical Report RR-2004-01, LIFO, Université d’Orléans (2003)Google Scholar
  7. 7.
    Limet, S., Salzer, G.: Proving properties of term rewrite systems via logic programs. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 170–184. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Limet, S., Saubion, F.: A general framework for R-unification. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 266–281. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1984)zbMATHGoogle Scholar
  10. 10.
    Lugiez, D., Schnoebelen, P.: The regular viewpoint on PA-processes. Theoretical Computer Science 274(1-2), 89–115 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable horn clauses, strongly recognizable relations and spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Information and Computation 147, 1–21 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142(1), 89–124 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Réty, P.: Regular sets of descendants for constructor-based rewrite systems. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol. 1705. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 270–273. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Sébastien Limet
    • 1
  • Pierre Pillot
    • 1
  1. 1.LIFOUniversité d’OrléansFrance

Personalised recommendations