Unification with Sequence Variables and Flexible Arity Symbols and Its Extension with Pattern-Terms

  • Temur Kutsia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


A minimal and complete unification procedure for a theory with individual and sequence variables, free constants and free fixed and flexible arity function symbols is described and a brief overview of an extension with pattern-terms is given.


Sequence Variable Function Symbol Equational Theory Symbolic Computation Free Semigroup 
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.
    H. Abdulrab and J.-P. Pécuchet. Solving word equations. J. Symbolic Computation, 8(5):499–522, 1990.CrossRefGoogle Scholar
  2. 2.
    F. Baader and W. Snyder. Unification theory. In A. Robinson and A. Voron-kov, editors, Handbook of Automated Reasoning, volume I, pages 445–532. Elsevier Science, 2001.Google Scholar
  3. 3.
    M. Benedikt, L. Libkin, T. Schwentick, and L. Segoufin. String operations in query languages. In Proceedings of the 20th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 2001.Google Scholar
  4. 4.
    B. Buchberger. Mathematica as a rewrite language. In T. Ida, A. Ohori, and M. Takeichi, editors, Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming), pages 1–13, Shonan Village Center, Japan, 1–4 November 1996. World Scientific.Google Scholar
  5. 5.
    B. Buchberger. Personal communication, 2001.Google Scholar
  6. 6.
    B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and W. Windsteiger. The Theorema project: A progress report. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000), pages 98–113, St.Andrews, 6–7 August 2000.Google Scholar
  7. 7.
    A. Colmerauer. An introduction to Prolog III. CACM, 33(7):69–91, 1990.Google Scholar
  8. 8.
    A. Farquhar, R. Fikes, and J. Rice. The Ontolingua Server: A tool for collaborative ontology construction. Int. J. of Human-Computer Studies, 46(6):707–727, 1997.CrossRefGoogle Scholar
  9. 9.
    M. R. Genesereth. Epilog for Lisp 2.0 Manual. Epistemics Inc., Palo Alto, 1995.Google Scholar
  10. 10.
    M. R. Genesereth and R. E. Fikes. Knowledge Interchange Format, Version 3.0 Reference Manual. Technical Report Logic-92-1, Computer Science Department, Stanford University, Stanford, June 1992.Google Scholar
  11. 11.
    S. Ginsburg and X. S. Wang. Pattern matching by Rs-operations: Toward a unified approach to querying sequenced data. In Proceedings of the 11th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 293–300, San Diego, 2–4 June 1992.Google Scholar
  12. 12.
    G. Grahne, M. Nykänen, and E. Ukkonen. Reasoning about strings in databases. In Proceedings of the Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 303–312, Minneapolis, 24–26 May 1994.Google Scholar
  13. 13.
    G. Grahne and E. Waller. How to make SQL stand for string query language. Lecture Notes in Computer Science, 1949:61–79, 2000.Google Scholar
  14. 14.
    M. Hamana. Term rewriting with sequences. In Proceedings of the First International Theorema Workshop, Hagenberg, Austria, 9–10 June 1997.Google Scholar
  15. 15.
    J. Jaffar. Minimal and complete word unification. J. of ACM, 37(1):47–85, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–298, Oxford, 1967. Pergamon Press. Appeared 1970.Google Scholar
  17. 17.
    T. Kutsia. Unification in a free theory with sequence variables and flexible arity symbols and its extensions. Technical report, RISC-Linz, 2002. Available from
  18. 18.
    A. Lentin. Equations in free monoids. In M. Nivat, editor, Automata, Languages and Programming, pages 67–85, Paris, 3–7 July 1972. North-Holland.Google Scholar
  19. 19.
    G. S. Makanin. The problem of solvability of equations on a free semigroup. Math. USSR Sbornik, 32(2), 1977.Google Scholar
  20. 20.
    G. Mecca and A. J. Bonner. Sequences, Datalog and transducers. In Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 23–35, San Jose, 22–25 May 1995.Google Scholar
  21. 21.
    F. Mora. Gröbner bases for non-commutative polynomial rings. In J. Calmet, editor, Proceedings of the 3rd International Conference on Algebraic Algorithms and Error-Correcting Codes (AAECC-3), volume 229 of LNCS, pages 353–362, Grenoble, July 1985. Springer Verlag.Google Scholar
  22. 22.
    R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation, 19:321–351, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    P. Hayes and C. Menzel. A semantics for the knowledge interchange format. Available from, 2001.
  24. 24.
    G. Plotkin. Building in equational theories. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 7, pages 73–90. Edinburgh University Press, 1972.Google Scholar
  25. 25.
    A. Rubio. Theorem proving modulo associativity. In Proceedings of the Conference of European Association for Computer Science Logic, LNCS, Paderborn, Germany, 1995. Springer Verlag.Google Scholar
  26. 26.
    K. U. Schulz. Word unification and transformation of generalized equations. J. Automated Reasoning, 11(2):149–184, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    J. Siekmann. String unification. Research paper, Essex University, 1975.Google Scholar
  28. 28.
    J. Siekmann. Unification and matching problems. Memo, Essex University, 1978.Google Scholar
  29. 29.
    M. Widera and C. Beierle. A term rewriting scheme for function symbols with variable arity. TR 280, Prakt. Informatik VIII, FernUniversitaet Hagen, 2001.Google Scholar
  30. 30.
    S. Wolfram. The Mathematica Book. Cambridge University Press and Wolfram Research, Inc., fourth edition, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Temur Kutsia
    • 1
    • 2
  1. 1.Research Institute for Symbolic ComputationJohannes Kepler University LinzLinzAustria
  2. 2.Software Competence Center HagenbergHagenbergAustria

Personalised recommendations