Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Artificial Intelligence, Automated Reasoning, and Symbolic Computation (AISC 2002, Calculemus 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2385))

Abstract

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.

Supported by the Austrian Science Foundation (FWF) under Project SFB F1302 and by Software Competence Center Hagenberg (Austria) under MathSoft project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Abdulrab and J.-P. Pécuchet. Solving word equations. J. Symbolic Computation, 8(5):499–522, 1990.

    Article  Google Scholar 

  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. 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. 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. B. Buchberger. Personal communication, 2001.

    Google Scholar 

  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. A. Colmerauer. An introduction to Prolog III. CACM, 33(7):69–91, 1990.

    Google Scholar 

  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.

    Article  Google Scholar 

  9. M. R. Genesereth. Epilog for Lisp 2.0 Manual. Epistemics Inc., Palo Alto, 1995.

    Google Scholar 

  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. 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. 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. 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. M. Hamana. Term rewriting with sequences. In Proceedings of the First International Theorema Workshop, Hagenberg, Austria, 9–10 June 1997.

    Google Scholar 

  15. J. Jaffar. Minimal and complete word unification. J. of ACM, 37(1):47–85, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  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. T. Kutsia. Unification in a free theory with sequence variables and flexible arity symbols and its extensions. Technical report, RISC-Linz, 2002. Available from ftp://ftp.risc.uni-linz.ac.at/pub/people/tkutsia/reports/unification.ps.gz.

  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. G. S. Makanin. The problem of solvability of equations on a free semigroup. Math. USSR Sbornik, 32(2), 1977.

    Google Scholar 

  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. 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. R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation, 19:321–351, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  23. P. Hayes and C. Menzel. A semantics for the knowledge interchange format. Available from http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIFIJCAI2001.pdf, 2001.

  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. 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. K. U. Schulz. Word unification and transformation of generalized equations. J. Automated Reasoning, 11(2):149–184, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  27. J. Siekmann. String unification. Research paper, Essex University, 1975.

    Google Scholar 

  28. J. Siekmann. Unification and matching problems. Memo, Essex University, 1978.

    Google Scholar 

  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. S. Wolfram. The Mathematica Book. Cambridge University Press and Wolfram Research, Inc., fourth edition, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Symbolic Computation, Johannes Kepler University Linz, A-4040, Linz, Austria

    Temur Kutsia

  2. Software Competence Center Hagenberg, Hauptstrasse 99, A-4232, Hagenberg, Austria

    Temur Kutsia

Authors
  1. Temur Kutsia
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany

    Jacques Calmet

  2. CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France

    Belaid Benhamou

  3. Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria

    Olga Caprotti

  4. ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France

    Laurent Henocque

  5. School of Computer Science, University of Birmingham, Birmingham, B15 2TT, UK

    Volker Sorge

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kutsia, T. (2002). Unification with Sequence Variables and Flexible Arity Symbols and Its Extension with Pattern-Terms. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-45470-5_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43865-6

  • Online ISBN: 978-3-540-45470-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation