Skip to main content
SpringerLink
Log in

Unification — Theory and Practice

  • Chapter
Logic Programming

  • 102 Accesses

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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.

Reference

  1. Abramson, H., Unification-Based Conditional Binding Constructs, Proceedings of the First International Logic Programming Conference, Marseille, France, September, 1982.

    Google Scholar 

  2. Abramson, H., A Prological Definition of HASL a Purely Functional Language with Unification Based Conditional Binding Expressions, New Generation Computing 2, 1 (1984).

    Google Scholar 

  3. Anderson, R. and Bledsoe, W. W., A Linear Format for Resolution with Merging and a New Technique For Establishing Completeness, Journal of the ACM 30, (1983), 525–534.

    Google Scholar 

  4. Bandes, R. G., Constraining-Unification and the Programming Language Unicorn, POPL, Salt Lake City, Utah, January, 1984.

    Google Scholar 

  5. Baxter, L. D., An Efficient Unification Algorithm, Technical Report CS-73–23, Applied Analysis and Computer Science Department, University of Waterloo, 1973.

    Google Scholar 

  6. Baxter, L. D., A Practical Linear Algorithm, Technical Report CS-76–13, Applied Analysis and Computer Science Department, University of Waterloo, 1976.

    Google Scholar 

  7. Berger-Sabbatel, G., Dang, W., Ianeselli, J. C. and Nguyen, G. T., Unification for a Prolog Data Base Machine, Proceedings of the Second International Logic Programming Conference, S. Tarnlund, ed., Uppsala University, Uppsala, Sweden, July 2–6, 1984, 207–218.

    Google Scholar 

  8. Chang, C. L. and Lee, R., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.

    MATH  Google Scholar 

  9. Chen, T. Y., Lassez, J. L. and Port, G. S., Maximal Unifiable Subsets and Minimal Non-unifiable Subsets, Report 84/16, Department of Computer Science, University of Melbourne, 1984.

    Google Scholar 

  10. Corbin, J. and Bidoit, M., A Rehabilitation of Robinson’s Unification Algorithm, in Information Processing 1988, R. E. Mason, (ed.), Elsevier, 1983, 627–636.

    Google Scholar 

  11. Cox, P. T., On Determining the Clauses of Non Unifiability, Technical Report, Department of Computer Science, Auckland University, 1982.

    Google Scholar 

  12. Digricoli, V. J., Resolution by Unification and Equality, Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas, 1979, 43–52.

    Google Scholar 

  13. Dilger, W. and Janson, A., Unification Graphs for Intelligent Backtracking in Deduction Symbols, Proceedings of GWAI 83, Dassel, Germany, 1983. Informatik-Fachbericht series.

    Google Scholar 

  14. Dilger, W. and Muller, J. P., Punify: An AI-Machine for Unification, in Proceedings of the 6th European Conference on Artificial Intelligence, T. O’shea, (ed.), Elsevier Publishing Company, Pisa, Italy, 1984.

    Google Scholar 

  15. Dwork, C., Kanellakis, P. C. and Mitchell, J. C., On The Sequential Nature Of Unification, The Journal Of Logic Programming 1, 1 (June 1984), 35–50.

    Article  MathSciNet  MATH  Google Scholar 

  16. Eder, E., Properties of Substitutions and Unifications, Proceedings of GWAI 83, Dassel, Germany, 1983. Informatik-Fachbericht series.

    Google Scholar 

  17. Eriksson, L., Synthesis Of A Unification Algorithm In a Logic Programming Calculus, The Journal Of Logic Programming 1,1 (June 1984), 3–18. Also available as UPMAIL Technical Report 22B.

    Article  MathSciNet  MATH  Google Scholar 

  18. Fages, F., Note sur l’Unification des Tremes de Premier Ordre Finis et Infinis, Technical Report, Institut National de Recherche en Informatique et en Automatique, France, 1984.

    Google Scholar 

  19. Fages, F., Associative-Commutative Unification, Technical Report No. 287, Institut National de Recherche en Informatique et en Automatique, 1984.

    Google Scholar 

  20. Fay, M. J., First-order unification in an equational theory, M.S. Thesis, Information Sciences Board, University of California at Santa Cruz, May 1978.

    Google Scholar 

  21. Fay, M. J., First-order unification in an equational theory, Proceedings of the Fourth Workshop on Automated Deduction, February 1979, 161–167.

    Google Scholar 

  22. Fishman, D. H. and Minker, J., Pi-Representation: A Clause Representation for Parallel Search, Artificial Intelligence 6, (1975), 103–127.

    Article  MathSciNet  MATH  Google Scholar 

  23. Fribourg, L., Oriented Equational Clauses as a Programming Language, The Journal Of Logic Programming 1, 2 (August 1984), 165–178.

    Article  MathSciNet  MATH  Google Scholar 

  24. Goguen, J. A. and Meseguer, J., Equality, Types, Modules and Generics for Logic Programming, Proceedings of the Second International Logic Programming Conference,S. Tarlund, ed., Uppsala University, Uppsala, Sweden, July 2–6, 1984, 115–126. Also as Technical Report, SRI, Stanford.

    Google Scholar 

  25. Haridi, S. and Sahlin, D., Efficient Implementation of Unification of Cyclic Structures, in Implementations of Prolog, J. A. Campbell, (ed.), Ellis Horwood, 1984.

    Google Scholar 

  26. Huet, G., Algebraic Aspects of Unification, Proceedings of Workshop on Automated Theorem Proving, Oberwolfach, Germany, 1976.

    Google Scholar 

  27. Itai, A. and Makowsky, J. A., Unification as a Complexity Measure for Logic Programming, Technical Report 301, Technion - Israel Institute of Technology, November 1983.

    Google Scholar 

  28. Jaffar, J., Efficient Unification Over Infinite Terms, New Generation Computing 2, 3 (January 1984). Also, Technical Report, Monash University, Clayton, Victoria, Australia.

    Google Scholar 

  29. Kahn, K. M., Uniform: A Language Based Upon Unification Which Unifies Much of LISP, Prolog and Act 1, Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, Canada, 1981.

    Google Scholar 

  30. Kapur, D.,Krishnamoorty, M. S. and Narendran, P., A New Linear Algorithm for Unification, Technical Report, General Electric, Schenectady, New York, 1982.

    Google Scholar 

  31. Kay, M., Unification in Grammar, Proceedings of an International Workshop on Natural Language Understanding and Logic Programming, University of Rennes, September, 1985.

    Google Scholar 

  32. Komorowsji, H. J. and Maluszynski, J., Unification-Free Execution of Logic Programs, Proceedings of the 2nd IEEE International Symposium on Logic Programming, Boston, USA, July, 1985.

    Google Scholar 

  33. Lassez, J. L. and Maher, M. J., The Semantics of Logic Programs,Oxford University Press,. In Preparation.

    Google Scholar 

  34. Lassez, J. L. and Maher, M. J., Antiunification, Technical Report 84–5, Department of Computer Science, University of Melbourne, Australia, 1984.

    Google Scholar 

  35. Levy, J., A Unification Algorithm For Concurrent Prolog, Proceedings of the Second International Logic Programming Conference,S. Tarnlund, ed., Uppsala University, Uppsala, Sweden, July 2–6, 1984, 331–342. Also available as a Technical Report from the Weizmann Institute of Science, Rechovot, Israel.

    Google Scholar 

  36. Maher, M. J., Semantics of Logic Programs, PhD Thesis, University of Melbourne, Department of Computer Science, 1985.

    Google Scholar 

  37. Maluszinski, J. andFullson, J. F,, A Notion of Grammatical Unification Applicable to Logic Programming Languages, Technical Report, University of Denmark, 1981.

    Google Scholar 

  38. Manna, Z. and Waldinger, R., Deductive Synthesis of the Unification Algorithm, Tech. Note 246, SRI International, July 1981.

    Google Scholar 

  39. Martelli, A. and Montanari, U., Unification in Linear Time and Space, Technical Report B76–16, University of Pisa, Italy, 1976.

    Google Scholar 

  40. Martelli, A. and Montanari, U., An Efficient Unification Algorithm, ACM Transactions on Programming Languages €1 Systems 4, 2 (1982), 258–282.

    Article  MATH  Google Scholar 

  41. Martelli, A. and Rossi, G., Efficient Unification With Infinite Terms In Logic Programming, International Conference On Fifth Generation Computer Systems,November 1984.

    Google Scholar 

  42. McCume, W. W., An Inference Mechanism For Resolution-style Theorem Provers, Master’s Thesis, Northwestern University, 1981.

    Google Scholar 

  43. Mills, P., A Systolic Unification Algorithm for VLSI, International Conference On Fifth Generation Computer Systems, November 1984.

    Google Scholar 

  44. Morokhovets, M. K., A Modified Unification Procedure, Cybernetics 20 20, 1 (1984), 147–152.

    MathSciNet  MATH  Google Scholar 

  45. Morris, J. B., E-resolution: Extension of Resolution to Include the Equality Relation, Proceedings of the International Joint Conference on Artificial Intelligence, Washington, D.C., May 79, 1969, 287–294.

    Google Scholar 

  46. Mukai, K., A Unification Algorithm for Infinite Trees, Proceedings of the International Joint Conference on Artificial Intelligence, Karlsruhe, Germany, 1983.

    Google Scholar 

  47. Naish, L. and Lassez, J. L., Most Specific Logic Programs, Technical Report 84/9, 1984.

    Google Scholar 

  48. Paterson, M. S. and Wegman, M. N., Linear Unification, Proceedings of the 8th ACM Symposium on the Theory of Computing, 1978. Also in Computer and System Sciences, Vol 16, 1978.

    Google Scholar 

  49. Pereira, F. C. N., A Structure-Sharing Representation for Unification-Based Grammar Formalisms, Proceedings of the 23rd Annual Meeting of the Association for Computational Linguistics, American Association for Computational Linguistics, July, 1985.

    Google Scholar 

  50. Raulefs, P., Siekmann, J., Szabo, P. and Unvericht, E., A Short Survey on the State of the Art in Matching and Unification Problems, AISB Quarterly 32, (December, 1978 ), 17–21.

    Google Scholar 

  51. Robinson, G. and Wos, L., Paramodulation and Theorem Proving in First Order Theories with Equality, Machine Intelligence 4, (1969), 135–150, American Elsevier.

    MathSciNet  MATH  Google Scholar 

  52. Robinson, J. A., Automatic Deduction with Hyper-resolution, International Journal of Computer Mathematics 1,(1965), 227-234.

    MATH  Google Scholar 

  53. Robinson, J. A., A review of automatic theorem proving, Proc. of the Symposia in Applied Mathematics 19,(1969), 1–18, American Mathematical Society.

    Google Scholar 

  54. Robinson, J. A., Computational Logic: the Unification Computation, Machine intelligence 6, (1971), 63–72.

    Google Scholar 

  55. Robinson, J. A., Fast Unification, Proceedings of Workshop on Automated Theorem Proving, Oberwolfach, Germany, 1976.

    Google Scholar 

  56. Robinson, J. A., Fundamentals of Machine-Oriented Deductive Logic, in Introductory Readings in Expert Systems, D. Michie, (ed.), Gordon and Breach, New York, 1982, 81–92.

    Google Scholar 

  57. Sato, M. and Sakurai, T., Qute: A Functional Language Based On Unification, International Conference On Fifth Generation Computer Systems, November 1984.

    Google Scholar 

  58. Sato, M. and Sakurai, T., QUTE: A Functional Language Based on Unification, in Logic Programming: Relations, Functions, and Equations, D. D. G. Lindstorm, (ed.), Prentice-Hall, Inc., Inglewood Cliffs, 1985.

    Google Scholar 

  59. Siekmann, J., Unification of Commutative Terms, in Symbolic and Algebraic Computation, E. W. Ng, (ed.), Springer-Verlag, 1979.

    Google Scholar 

  60. Siekmann, J. and Szabo, P., Universal Unification and a Classification of Equational Theories, in Lecture Notes in Computer Science - 188, W. Walhster, (ed.), Springer Verlag, 1982, 102–141.

    Google Scholar 

  61. Smolka, G., Fresh: A Higher-Order Language with Unification and Multiple Results, in Logic Programming: Relations, Functions, and Equations, D. D. G. Lindstrom, (ed.), Prentice-Hall, Inc., Inglewood Cliffs, 1985.

    Google Scholar 

  62. Stickel, M. E., A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM 28, 3 (1981), 423–434.

    Article  MathSciNet  MATH  Google Scholar 

  63. Trum, P. and Winterstein, G., Description and Practical Comparison of Unification Algorithms, Technical Report, University of Kaiserslautern, Germany, 1978.

    Google Scholar 

  64. Vitter, J. S. and Simons, R. A., Parallel Algorithms for Unification and other Complete Problems in P, in Proc ACM-84, October 1984, 75–84.

    Google Scholar 

  65. Winterstein, G., Pradikatenlogik-Programme mit Evaluierbare Functionen, Technical Report, Doctoral Dissertation, University of Kaiserslautern, Germany, 1978.

    Google Scholar 

  66. Winterstein, G., Dausman, M. and Persch, G., Deriving Different Unification Algorithms from a Specification in Logic, in Workshop on Logic Programming, S. Tarnlund, (ed.), Debrecen, Hungary, July 1980.

    Google Scholar 

  67. Wolfram, D. A., Maher, M. J. and Lassez, J. L., A Unified Treatment of Resolution Strategies for Logic Programs, Proceedings of the 2nd International Logic Programming Conference, Sweden, July 2–6, 1984. Also Technical Report 83/12, Dept. of Computer Science, University of Melbourne, 36 pp.

    Google Scholar 

  68. Woo, N., A Hardware Unification Unit: Design and Analysis, Proceedings of the 12th International Symposium on Computer Architecture, Boston, June, 1985.

    Google Scholar 

  69. Wrightson, G., Semantic Tableaux, Unification and Links, Technical Report, CSD-ANZARP-84–001, May, 1984.

    Google Scholar 

  70. Yasuura, H., On Parallel Computational Complexity Of Unifiçation, International Conference On Fifth Generation Computer Systems, November 1984. Also, Technical Report TR-0027, ICOT - Institute for New Generation Computer Technology, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Melbourne, 3052, Parkville, Victoria, Australia

    Isaac Balbin

  2. Computer Science Department, University of California, 90024, Los Angeles, California, USA

    Koenraad Lecot

Authors
  1. Isaac Balbin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Koenraad Lecot
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Isaac Balbin and Koenraad Lecot

About this chapter

Cite this chapter

Balbin, I., Lecot, K. (1985). Unification — Theory and Practice. In: Logic Programming. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-5044-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-94-009-5044-3_3

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-0-908069-15-6

  • Online ISBN: 978-94-009-5044-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation