Many-sorted unification

ABSTRACT

Many-sorted unification is considered; that is, unification in the many-sorted free algebras of terms, where variables, as well as the domains and ranges of functions, are restricted to certain subsets of the universe, given as a potentially infinite hierarchy of sorts. It is shown that complete and minimal sets of unifiers may not always exist for many-sorted unification. Conditions for sort hierarchies that are equivalent for the existence of these sets with one, finitely many, or infinitely many elements are presented. It is also proved that being a forest-structured sort hierarchy is a necessary and sufficient criterion for the Robinson Unification Theorem to hold for many-sorted unification. An algorithm for many-sorted unification is given.

REFERENCES

• 1: BIRKHOFF, G. Lattice Theory. Vol. 25, American Mathematical Society Colloquium Publications, Providence, R.I., 1967.
• 2: COHN, P.M. Universal Algebra. Reidel, Dordrecht, 1981.
• 3: CUNNINGHAM, R. J., AND DICK, A. J.J. Rewrite systems on a lattice of types. Acta Inf. 22, 2 (1985), 149-169.
• 4: Veronica Dahl, Translating Spanish into logic through logic, Computational Linguistics, v.7 n.3, p.149-164, July-September 1981
• 5: Elmar Eder, Properties of substitutions and unifications, Journal of Symbolic Computation, v.1 n.1, p.31-46, March 1985 [doi>10.1016/S0747-7171(85)80027-4]
• 6: François Fages , Gérard P. Huet, Complete Sets of Unifiers and Matchers in Equational Theories, Proceedings of the 8th Colloquium on Trees in Algebra and Programming, p.205-220, March 09-11, 1983
• 7: Alan M. Frisch, An investigation into inference with restricted quantification and a taxonomic representation, ACM SIGART Bulletin [doi>10.1145/1056541.1056546]
• 8: FRISCH, A.M. Parsing with restricted quantification. In Proceedings of the Society for the Study of Artificial Intelligence and Simulation of Behavior Conference, 1985.
• 9: Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Operational Semantics for Order-Sorted Algebra, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.221-231, July 15-19, 1985
• 10: GOGUEN, J. A., THATCHER, J. W., AND WAGNER, E. G. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, vol. 4, R. T. Yeh, Ed. Prentice-Hall, Englewood Cliffs, N.J., 1978, pp. 80-321.
• 11: HEROLD, A. Some basic notions of first-order unification theory. Interner Bericht 15/83, Universitiit Karlsruhe, Institut flit Informatik I, 1983.
• 12: HUET, G., AND OPPEN, D.C. Equations and rewrite rules: A survey. Tech. Rep. CSL-111, SRI International, Menlo Park, Calif., 1980; also in Formal Languages Theory: Perspectives and Open Problems, R. Book, Ed. Academic Press, Orlando, Fla., 1980, pp. 349-405.
• 13: IRANI, K. B., AND SHIN, D.G. A many-sorted resolution based on an extension of a first-order language. In Proceedings of the 9th International Joint Conference on Artificial Intelligence (Los Angeles, Calif.). Morgan Kaufmann, Los Altos, Calif., 1985, pp. 1175-1177.
• 14: KNUTH, D., AND BENDIX, P. Simple word problems in universal algebras. In Computational Problems in Abstract Algebras, J. Leech, Ed. Pergamon, Oxford, England, 1970.
• 15: MACNEILLE, H.M. Partially ordered sets. Trans. Am. Math. Soc. 42 (1937), 416-460.
• 16: PLOTKIN, G. Building-in equational theories. Mach. Intell. 7 (1972), 73-90.
• 17: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 18: SCHMIDT-SCHAUSS, M. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. In Proceedings of the 9th International Joint Conference on Artificial Intelligence (LOs Angeles, Calif.). Morgan Kaufmann, LOs Altos, Calif., 1985, pp. i 162-1168.
• 19: M Schmidt-Schauss, Unification in many-sorted equational theories, Proc. of the 8th international conference on Automated deduction, p.538-552, August 1986, Oxford, United Kingdom
• 20: Jörg H. Siekmann, Universal Unification, Proceedings of the 7th International Conference on Automated Deduction, p.1-42, May 14-16, 1984
• 21: SIEKMANN, J., AND WRIGHTSON, G., EDS. Automation of Reasoning--Classical Papers on Computational Logic. Vols. 1 & 2, Springer-Vedag, Berlin, 1983.
• 22: STICKEL, M.E. Automated deduction by theory resolution. In Proceedings of the 9th International Joint Conference on Artificial Intelligence (LOs Angeles, Calif.). Morgan Kaufmann, LOs Altos, Calif., 1985, pp. 1181-1186; revised version in J. Autom. Reasoning 1, 4 (1985), 333-355.
• 23: Mark E. Stickel, Schubert's steamroller problem: formulations and solutions, Journal of Automated Reasoning, v.2 n.1, p.89-101, 1986
• 24: WALTHER, C. A many-sorted calculus based on resolution and paramodulation. In Proceedings of the 8th International Joint Conference on Artificial Intelligence (Karlsruhe). Morgan Kaufmann, Los Altos, Calif., 1983, pp. 882-891.
• 25: WALTHER, C. Unification in many-sorted theories. In Proceedings of the 6th European Conference on Artificial Intelligence (Pisa, Italy). North-Holland, Amsterdam, 1985, pp. 593-602; also in Advances in Artificial Intelligence, T. O'Shea, Ed. North-Holland, Amsterdam, 1985, pp. 383-392.
• 26: Christoph Walther, A mechanical solution of Schubert's steamroller by many-sorted resolution, Artificial Intelligence, v.26 n.2, p.217-224, May 1985 [doi>10.1016/0004-3702(85)90029-3]
• 27: WALTHER, C. A classification of unification problems in many-sorted theories. Intemer Bericht 10/85, Universitat Karlsruhe, Institiit f'tir Informatik, I, 1985.
• 28: C. Walther, A many-sorted calculus based on resolution and paramodulation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1987
• 29: Wos, L., AND ROBINSON, G. Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving. In Wordproblems, W. W. Boone, F. B. Cannonito, and R. C. Lyndon, Eds. North-Holland, Amsterdam, 1973; also in {21}.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Pattern matching

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Substitution mechanisms**
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Resolution

General Terms:
Algorithms, Theory, Verification