An Efficient Unification Algorithm

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An Efficient Unification Algorithm

Full text

Pdf (1.26 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 4 , Issue 2 (April 1982) table of contents

Pages: 258 - 282

Year of Publication: 1982

ISSN:0164-0925

Authors

Alberto Martelli	Istituto di Scienze della Informazione, Università di Torino, Corso M. d'Azeglio 42, I-10125 Torino, Italy
Ugo Montanari	Istituto di Scienze della Informazione, Università di Pisa, Corso Italia 40, I-56100 Pisa, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 31, Downloads (12 Months): 266, Citation Count: 77

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/357162.357169 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
	2	BAXTER, L.D. A practically linear unification algorithm. Res. Rep. CS-76-13, Dep. of Applied Analysis and Computer Science, Univ. of Waterloo, Waterloo, Ontario, Canada.
	3	BOYER, R.S., AND MOORE, J.S. The sharing of structure in theorem-proving programs. In Machine Intelligence, vol. 7, B. Meltzer and D. Michie (Eds.). Edinburgh Univ. Press, Edinburgh, Scotland, 1972, pp. 101-116.
	4	R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
	5	CHiNa, C.L., AND LEE, R.C. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.
	6	HEwn~r, C. Description and Theoretical Analysis (Using Schemata) of PLANNER: A Language for Proving Theorems and Manipulating Models in a Robot. Ph.D. dissertation, Dep. of Mathematics, Massachusetts Institute of Technology, Cambridge, Mass., 1972.
	7	HUET, G. R~solution d'bquations dans les langages d'ordre 1, 2 ..... w. Th~se d'~tat, Sp~cialit~ Math~matiques, Universit~ Paris VII, 1976.
	8	HUET, G.P. A unification algorithm for typed h-calculus. Theor. Comput. Sci. 1, I (June 1975), 27-57.
	9	KNUT~, D.E., ANn BENDIX, P.B. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech (Ed.). Pergamon Press, Elmsford, N.Y., 1970, pp. 263-297.
	10	KowALsKI, R. Predicate logic as a programming language. In Information Processing 74, Elsevier North-Holland, New York, 1974, pp. 569-574.
	11	LEVI, G., AND SIROVICH, F. Proving program properties, symbolic evaluation and logical procedural semantics. In Lecture Notes in Computer Science, vol. 32: Mathematical Foundations of Computer Science 1975. Springer-Verlag, New York, 1975, pp. 294-301.
	12	MARTELLI, A., AND MONTANARI, U. Theorem proving with structure sharing and efficient unification. Internal Rep. S-77-7, Ist. di Scienze della Informazione, University of Pisa, Pisa, Italy; also in Proceedings of the 5th International Joint Conference on Artificial Intelligence, Boston, 1977, p. 543.
	13	MARTELLI, A., AND MONTANARI, U. Unification in linear time and space: A structured presentation. Internal Rep. B76-16, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy, July 1976.
	14	MmNER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3 (Dec. 1978), 348-375.
	15	PATERSON, M.S., AND WEaMAN, M.N. Linear unification. J. Comput. Syst. Sci. 16, 2 (April 1978), 158-167.
	16	ROBINSON, J.A. Fast unification. In Theorem Proving Workshop, Oberwolfach, W. Germany, Jan. 1976.
	17	ROBINSON, J.A. Computational logic: The unification computation. In Machine Intelligence, vol. 6, B. Meltzer and D. Michie (Eds.). Edinburgh Univ. Press, Edinburgh, Scotland, 1971, pp. 63-72.
	18	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]
	19	SHORTLIFFE, E.H. Computer-Based Medical Consultation: MYCIN. Elsevier North-Holland, New York, 1976.
	20	STICKEL, M.E. A complete unification algorithm for associative-commutative functions. In Proceedings of the 4th International Joint Conference on Artificial Intelligence, Tbilisi, U.S.S.R., 1975, pp. 71-76.
	21	TRUM, P., AND WINTERSTEIN, G. Description, implementation, and practical comparison of unification algorithms. Internal Rep. 6/78, Fachbereich Informatik, Univ. of Kaiserlautern, W. Germany.
	22	VENTURINI ZILLI, M. Complexity of the unification algorithm for first-urder expressions. Calcolo 12, 4 (Oct.-Dec. 1975), 361-372.
	23	Friedrich W. von Henke , David C. Luckham, Automatic program verification III: a methodology for verifying programs., Stanford University, Stanford, CA, 1974
	24	WALOINOER, R.J., AND LEVITt, K.N. Reasoning about programs. Artif Intell. 5, 3 (Fall 1974), 235-316.
	25	David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.109-115, August 15-17, 1977

CITED BY 77

	P. C. Kanellakis , J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-115, January 11-13, 1989, Austin, Texas, United States
	R. Ramesh , I. V. Ramakrishnan , D. S. Warren, Automata-driven indexing of Prolog clauses, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.281-291, December 1989, San Francisco, California, United States
	Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996
	F. N. Sibai , L. Watson , M. Lu, Design and performance measurements of a parallel machine for the unification algorithm, ACM SIGMICRO Newsletter, v.20 n.3, p.21-30, Sep. 1989
	P. L. Civera , F. Maddaleno , G. L. Piccinini , M. Zamboni, An experimental VLSI Prolog interpreter: preliminary measurements and results, Proceedings of the 14th annual international symposium on Computer architecture, p.117-126, June 02-05, 1987, Pittsburgh, Pennsylvania, United States
	Stefaan Decorte , Danny De Schreye , Henk Vandecasteele, Constraint-based termination analysis of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1137-1195, Nov. 1999
	Reinhard Pichler, On the complexity of equational problems in CNF, Journal of Symbolic Computation, v.36 n.1-2, p.235-269, July 2003
	Alexis Koster, Compiling prolog programs for parallel execution on a cellular machine, Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge, p.167-178, January 1984
	Johan Nordlander, Pragmatic subtyping in polymorphic languages, ACM SIGPLAN Notices, v.34 n.1, p.216-227, Jan. 1999
	Fritz Henglein, Type inference and semi-unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.184-197, July 25-27, 1988, Snowbird, Utah, United States
	Giorgio Levi , Fausto Spoto, Non pair-sharing and freeness analysis through linear refinement, ACM SIGPLAN Notices, v.34 n.11, p.52-61, Nov. 1999
	Seif Haridi , Peter Van Roy , Per Brand , Michael Mehl , Ralf Scheidhauer , Gert Smolka, Efficient logic variables for distributed computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.569-626, May 1999
	Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993
	James A. Brown , Ramiro Guerreiro, APL2 implementations of unification, ACM SIGAPL APL Quote Quad, v.17 n.4, p.216-225, May 1987
	David McAllester, On the complexity analysis of static analyses, Journal of the ACM (JACM), v.49 n.4, p.512-537, July 2002
	Gyula Magó, Data sharing in an FFP machine, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.201-207, August 15-18, 1982, Pittsburgh, Pennsylvania, United States
	Kevin Knight, Unification: a multidisciplinary survey, ACM Computing Surveys (CSUR), v.21 n.1, p.93-124, March 1989
	Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and expressive power of logic programming, ACM Computing Surveys (CSUR), v.33 n.3, p.374-425, September 2001
	Krzysztof R. Apt , Alessandro Pellegrini, On the occur-check-free PROLOG programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.687-726, May 1994
	Michael R. Levy, Type checking, separate compilation and reusability, ACM SIGPLAN Notices, v.19 n.6, p.285-289, June 1984
	Jean Gallier , Paliath Narendran , Stan Raatz , Wayne Snyder, Theorem proving using equational matings and rigid E-unification, Journal of the ACM (JACM), v.39 n.2, p.377-430, April 1992
	P. A. Subrahmanyam , J-H. You, Pattern driven lazy reduction: A unifying evaluation mechanism for functional and logic programs, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.228-234, January 15-18, 1984, Salt Lake City, Utah, United States
	Reinhard Pichler, Explicit versus implicit representations of subsets of the Herbrand universe, Theoretical Computer Science, v.290 n.1, p.1021-1056, 1 January 2003
	Ana Bove, Simple general recursion in type theory, Nordic Journal of Computing, v.8 n.1, p.22-42, Spring 2001
	Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida
	Sushil Jajodia , Pierangela Samarati , Maria Luisa Sapino , V. S. Subrahmanian, Flexible support for multiple access control policies, ACM Transactions on Database Systems (TODS), v.26 n.2, p.214-260, June 2001
	Colin Runciman , Ian Toyn, Retrieving re-usable software components by polymorphic type, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.166-173, September 11-13, 1989, Imperial College, London, United Kingdom
	Agostino Dovier , Carla Piazza , Enrico Pontelli , Gianfranco Rossi, Sets and constraint logic programming, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.5, p.861-931, Sept. 2000
	J. I. Glasgow , M. A. Jenkins , E. Blevis , M. P. Féret, Logic Programming with Arrays, IEEE Transactions on Knowledge and Data Engineering, v.3 n.3, p.307-319, September 1991
	María García de la Banda , Manuel Hermenegildo , Kim Marriott, Independence in CLP languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.296-339, March 2000
	Pierluigi Civera , Gianluca Piccinini , Maurizio Zamboni, Implementation Studies for a VLSI Prolog Coprocessor, IEEE Micro, v.9 n.1, p.10-23, January 1989
	Giorgio Levi , Fausto Spoto, Pair-independence and freeness analysis through linear refinement, Information and Computation, v.182 n.1, p.14-52, 10 April 2003
	Marco Bellia , M. Eugenia Occhiuto, N-axioms parallel unification, Fundamenta Informaticae, v.55 n.2, p.115-128, May 2003
	Fernando Pereira, Review of "The logic of typed feature structures" by Bob Carpenter. Cambridge University Press 1992., Computational Linguistics, v.19 n.3, September 1993
	M. Garcia de la Banda , M. Hermenegildo , M. Bruynooghe , V. Dumortier , G. Janssens , W. Simoens, Global analysis of constraint logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.5, p.564-614, Sept. 1996
	Didier Rémy, Projective ML, ACM SIGPLAN Lisp Pointers, v.V n.1, p.66-75, Jan. 1992
	Stavros Tripakis , Christos Sofronis , Paul Caspi , Adrian Curic, Translating discrete-time simulink to lustre, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.4, p.779-818, November 2005
	F. N. Sibai , K. L. Watson , Mi Lu, A Parallel Unification Machine, IEEE Micro, v.10 n.4, p.21-33, July 1990
	Micheal Kifer , Eliezer L. Lozinskii, SYGRAF: Implementing Logic Programs in a Database Style, IEEE Transactions on Software Engineering, v.14 n.7, p.922-935, July 1988
	Ken Kaneiwa, Order-sorted logic programming with predicate hierarchy, Artificial Intelligence, v.158 n.2, p.155-188, October 2004
	Venkatesh Choppella , Christopher T. Haynes, Source-tracking unification, Information and Computation, v.201 n.2, p.121-159, September 15, 2005
	Christian Urban , Andrew M. Pitts , Murdoch J. Gabbay, Nominal unification, Theoretical Computer Science, v.323 n.1-3, p.473-497, 14 September 2004
	Khalil Djelloul, Decomposable theories, Theory and Practice of Logic Programming, v.7 n.5, p.583-632, September 2007
	Khalil Djelloul , Thi-Bich-Hanh Dao, Solving first-order constraints in the theory of finite or infinite trees: introduction to the decomposable theories, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
	Martin Plümicke , Jörg Bäuerle, Typeless programming in Java 5.0, Proceedings of the 4th international symposium on Principles and practice of programming in Java, August 30-September 01, 2006, Mannheim, Germany
	Steven Eker , Narciso Martí-Oliet , José Meseguer , Alberto Verdejo, Deduction, Strategies, and Rewriting, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.11, p.3-25, July, 2007
	Didier Rémy , Boris Yakobowski, A graphical presentation of ML^F types with a linear-time unification algorithm, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
	Kumar Neeraj Verma , Jean Goubault-Larrecq, Alternating two-way AC-tree automata, Information and Computation, v.205 n.6, p.817-869, June, 2007
	Clark Barrett , Igor Shikanian , Cesare Tinelli, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.8, p.23-37, June, 2007
	Brad Lushman , Gordon V. Cormack, A larger decidable semiunification problem, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
	Agostino Dovier , Enrico Pontelli , Gianfranco Rossi, Set unification, Theory and Practice of Logic Programming, v.6 n.6, p.645-701, November 2006
	Barbara Morawska, General E-unification with Eager Variable Elimination and a Nice Cycle Rule, Journal of Automated Reasoning, v.39 n.1, p.77-106, July 2007
	Alexander Serebrenik , Danny Schreye, Termination of Floating-Point Computations, Journal of Automated Reasoning, v.34 n.2, p.141-177, December 2005
	N. Peltier, Representing and Building Models for Decidable Subclasses of Equational Clausal Logic, Journal of Automated Reasoning, v.33 n.2, p.133-170, September 2004
	Gopalan Nadathur, A treatment of higher-order features in logic programming, Theory and Practice of Logic Programming, v.5 n.3, p.305-354, May 2005
	Uwe Egly , Reinhard Pichler , Stefan Woltran, On Deciding Subsumption Problems, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.255-294, January 2005
	Hubert Comon , Mehmet Dincbas , Jean-Pierre Jouannaud , Claude Kirchner, A Methodological View of Constraint Solving, Constraints, v.4 n.4, p.337-361, December 1999
	Gérard Boudol, The recursive record semantics of objects revisited, Journal of Functional Programming, v.14 n.3, p.263-315, May 2004
	Patricia M. Hill , Roberto Bagnara , Enea Zaffanella, Soundness, idempotence and commutativity of set-sharing, Theory and Practice of Logic Programming, v.2 n.2, p.155-201, March 2002
	Dieter Hutter, Coloring Terms to Control Equational Reasoning, Journal of Automated Reasoning, v.18 n.3, p.399-442, June 1997
	Michael Hanus , Christian Prehofer, Higher-order narrowing with definitional trees, Journal of Functional Programming, v.9 n.1, p.33-75, January 1999
	Li Dafa, Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving, Journal of Automated Reasoning, v.18 n.1, p.105-134, February 1997
	Martin Plümicke, Typeless programming in Java 5.0 with wildcards, Proceedings of the 5th international symposium on Principles and practice of programming in Java, September 05-07, 2007, Lisboa, Portugal
	Jan Van den Bussche , Stijn Vansummeren, Polymorphic type inference for the named nested relational calculus, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.3-es, December 2007
	Andrea Pugliese , Octavian Udrea , V. S. Subrahmanian, Scaling RDF with Time, Proceeding of the 17th international conference on World Wide Web, April 21-25, 2008, Beijing, China
	Stéphanie Delaune , Pascal Lafourcade , Denis Lugiez , Ralf Treinen, Symbolic protocol analysis for monoidal equational theories, Information and Computation, v.206 n.2-4, p.312-351, February, 2008
	Andreas Stolcke, Unification as constraint satisfaction in structured connectionist networks, Neural Computation, v.1 n.4, p.559-567, Winter 1989
	Khalil Djelloul , Thi-bich-hanh Dao , Thom FrÜhwirth, Theory of finite or infinite trees revisited, Theory and Practice of Logic Programming, v.8 n.4, p.431-489, July 2008
	Helmut Seidl , Kumar Neeraj Verma, Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying, ACM Transactions on Computational Logic (TOCL), v.9 n.4, p.1-45, August 2008
	Véronique Cortier , Stéphanie Delaune, Safely composing security protocols, Formal Methods in System Design, v.34 n.1, p.1-36, February 2009
	Keehang Kwon , Dae-Seong Kang , Jinsoo Kim, A Query System for Texts with Macros, IEICE - Transactions on Information and Systems, v.E91-D n.1, p.145-147, January 2008
	Ginés Moreno , Vicente Pascual, A hybrid programming scheme combining fuzzy-logic and functional-logic resources, Fuzzy Sets and Systems, v.160 n.10, p.1402-1419, May, 2009
	Pascual Julián-Iranzo , Clemente Rubio-Manzano , Juan Gallardo-Casero, Bousi~Prolog: a Prolog Extension Language for Flexible Query Answering, Electronic Notes in Theoretical Computer Science (ENTCS), 248, p.131-147, August, 2009
	Ofer Arieli , Marc Denecker , Bert Van Nuffelen , Maurice Bruynooghe, Coherent integration of databases by abductive logic programming, Journal of Artificial Intelligence Research, v.21 n.1, p.245-286, January 2004
	Takahira Yamaguchi , Yoshikazu Tezuka , Osamu Kakusho, Parallel processing of resolution, Proceedings of the 9th international joint conference on Artificial intelligence, p.1178-1180, August 18-23, 1985, Los Angeles, California
	Kuniaki Mukai, A unification algorithm for infinite trees, Proceedings of the Eighth international joint conference on Artificial intelligence, p.547-549, August 08-12, 1983, Karlsruhe, West Germany
	María Alpuente , Santiago Escobar , José Meseguer , Pedro Ojeda, Order-Sorted Generalization, Electronic Notes in Theoretical Computer Science (ENTCS), 246, p.27-38, August, 2009