Unification with Sequence Variables and Flexible Arity Symbols and Its Extension with Pattern-Terms
- 225 Downloads
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.
KeywordsSequence Variable Function Symbol Equational Theory Symbolic Computation Free Semigroup
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- 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