Alberto Martelli
- 1 ARo, A.V., HoPcRoPr, J.E., A~D ULLMAN, J.D. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 4 BURSTALL, R.M., AND DARLINGTON, J. A transformation system for developing recursive programs. J. ACM 24, 1 (Jan. 1977), 44-67. Google Scholar
- 5 CHiNa, C.L., AND LEE, R.C. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 8 HUET, G.P. A unification algorithm for typed h-calculus. Theor. Comput. Sci. 1, I (June 1975), 27-57.Google Scholar
- 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.Google Scholar
- 10 KowALsKI, R. Predicate logic as a programming language. In Information Processing 74, Elsevier North-Holland, New York, 1974, pp. 569-574.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 14 MmNER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3 (Dec. 1978), 348-375.Google Scholar
- 15 PATERSON, M.S., AND WEaMAN, M.N. Linear unification. J. Comput. Syst. Sci. 16, 2 (April 1978), 158-167.Google Scholar
- 16 ROBINSON, J.A. Fast unification. In Theorem Proving Workshop, Oberwolfach, W. Germany, Jan. 1976.Google Scholar
- 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.Google Scholar
- 18 ROBINSON, J.A. A machine-oriented logicbased on the resolution principle. J. ACM 12, i (Jan. 1965), 23-41. Google Scholar
- 19 SHORTLIFFE, E.H. Computer-Based Medical Consultation: MYCIN. Elsevier North-Holland, New York, 1976.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 22 VENTURINI ZILLI, M. Complexity of the unification algorithm for first-urder expressions. Calcolo 12, 4 (Oct.-Dec. 1975), 361-372.Google Scholar
- 23 YON HENKE, F.W., AND LUCKHAM, D.C. Automatic program verificationIII: A methodology for verifying programs. Stanford Artificial Intelligence Laboratory Memo AIM-256, Stanford Univ., Stanford, Calif., Dec. 1974. Google Scholar
- 24 WALOINOER, R.J., AND LEVITt, K.N. Reasoning about programs. Artif Intell. 5, 3 (Fall 1974), 235-316.Google Scholar
- 25 WARREN, D.H.D., PEREIRA, L.M., AND PEREIRA, F. PROLOG--The language and its implementation compared with LISP. In Proceedings of Symposium on Artificial Intelligence and Programming Languages, Univ. of Rochester, Rochester, N.Y., Aug. 15-17, 1977. Appeared as joint issue: SIGPLAN Notices (ACM) 12, 8 (Aug. 1977), and SIGART Newsl. 64 (Aug. 1977), 109-115. Google Scholar
Index Terms
- An Efficient Unification Algorithm
Recommendations
Unification nets: canonical proof net quantifiers
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceProof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's ...
Functions-as-constructors higher-order unification: extended pattern unification
AbstractUnification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, ...
Comments