×

Higher-order unification revisited: Complete sets of transformations. (English) Zbl 0682.03034

Some approach to higher-order unification is presented. The approach is based on the method of transformation of terms and extends the approach developed by Martelli and Montanari in the context of first-order unification. The method of transformations for solving unification problems is much like the well-known Gaussian method used for solving systems of linear equations. Gaussian elimination and first-order unification are somewhat similar. But in the higher-order case the analogy breaks down. The most important differences to the first-order case have to do with the imitation rule and the generalization of the notion of a partial binding to higher-order substitutions.
Reviewer: N.Zamov

MSC:

03F35 Second- and higher-order arithmetic and fragments
03B35 Mechanization of proofs and logical operations

Software:

ETPS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews, P. B., Resolution in Type Theory, JSL, 36, 3, 414-432 (1971) · Zbl 0231.02038
[2] Andrews, P. B., Theorem Proving via General Matings, JACM, 28, 2, 193-214 (1981) · Zbl 0456.68119
[3] Andrews, P. B.; Miller, D.; Cohen, E.; Pfenning, F., Automating Higher-Order Logic, Contemporary Mathematics, 29, 169-192 (1984)
[4] Andrews, P. B., (An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (1986), Academic Press, Inc.) · Zbl 0617.03001
[5] Barendregt, H. P., (The Lambda Calculus (1984), North-Holland) · Zbl 0549.03012
[6] Church, A., A Formulation of the Simple Theory of Types, JSL, 5, 56-68 (1940) · JFM 66.1192.06
[7] Darlington, J. L., A Partial Mechanization of Second-Order Logic, Machine Intelligence, 6, 91-100 (1971) · Zbl 0261.68041
[8] Elliot, C.; Pfenning, F., A Family of Program Derivations for Higher-Order Unification, (Ergo Report 87-045 (November 1987), CMU)
[9] Elliot, C., Higher-Order Unification with Dependent Function Types, (Proceedings of the Third RTA (1989))
[10] Fages, F.; Huet, G., Complete Sets of Unifiers and Matchers in Equational Theories, TCS, 43, 189-200 (1986) · Zbl 0615.03002
[11] Farmer, W., Length of Proofs and Unification Theory, (Ph.D. Thesis (1984), University of Wisconsin—Madison)
[12] Farmer, W., A Unification Algorithm for Second-Order Monadic Terms, Annals of Pure and Applied Logic, 39, 131-174 (1988) · Zbl 0655.03004
[13] Farmer, W., “Simple Second-Order Languages for which Unification is Undecidable,” Unpublished Technical Report, MITRE Corporation, Bedford, MA (submitted for publication).; Farmer, W., “Simple Second-Order Languages for which Unification is Undecidable,” Unpublished Technical Report, MITRE Corporation, Bedford, MA (submitted for publication). · Zbl 0731.03005
[14] Farmer, W., “A Unification-Theoretic Method for Investigating the \(k\); Farmer, W., “A Unification-Theoretic Method for Investigating the \(k\) · Zbl 0735.03001
[15] Felty, A.; Miller, D., Specifying Theorem Provers in a Higher-Order Logic Programming Language, (Ninth International Conference on Automated Deduction. Ninth International Conference on Automated Deduction, Argonne, Illinois (1988)) · Zbl 0645.68097
[16] Gallier, J. H., (Logic for Computer Science: Foundations of Automatic Theorem Proving (1986), Harper and Row: Harper and Row New York) · Zbl 0605.03004
[17] Gallier, J. H.; Snyder, W., A General Complete E-Unification Procedure (1987), RTA: RTA Bordeaux · Zbl 0641.68045
[18] Gallie, J. H.; Snyder, W., Complete Sets of Transformations for General \(E\)-Unification (1989), to appear in TCS
[19] Goldfarb, W., The Undecidability of the Second-Order Unification Problem, TCS, 13, 2, 225-230 (1981) · Zbl 0457.03006
[20] Gould, W. E., A Matching Procedure for Omega-Order Logic, (Ph.D. Thesis (1966), Princeton University)
[21] Guard, J.R., “Automated Logic for Semi-Automated Mathematics,” Scientific Report 1, AFCRL 64-411, Contract AF 19 (628)-3250 AD 602 710.; Guard, J.R., “Automated Logic for Semi-Automated Mathematics,” Scientific Report 1, AFCRL 64-411, Contract AF 19 (628)-3250 AD 602 710. · Zbl 0175.28205
[22] Guard, J.; Oglesby, J.; Settle, L., Semi-Automated Mathematics, JACM, 16, 49-62 (1969) · Zbl 0175.28205
[23] Hannan, J.; Miller, D., Enriching a Meta-Language with Higher-Order Features, (Workshop on Meta-Programming in Logic Programming. Workshop on Meta-Programming in Logic Programming, Bristol (1988))
[24] Hannan, J.; Miller, D., Uses of Higher-Order Unification for Implementing Program Transformers, (Fifth International Conference on Logic Programming (1988), MIT Press)
[25] Herbrand, J., “Sur la Théorie de la Démonstration,” in: Logical Writings; Herbrand, J., “Sur la Théorie de la Démonstration,” in: Logical Writings
[26] Hindley, J.; Seldin, J., (Introduction to Combinators and Lambda Calculus (1986), Cambridge University Press) · Zbl 0614.03014
[27] Huet, G., A Mechanization of Type Theory, (Proceedings of the Third International Joint Conference on Artificial Intelligence (1973)), 139-146
[28] Huet, G., A Unification Algorithm for Typed λ-Calculus, TCS, 1, 27-57 (1975) · Zbl 0337.68027
[29] Huet, G., Résolution d’Equations dans les Langages d’Ordre 1,2,…,ω, (Thèse d’Etat, VII (1976), Université de Paris)
[30] Huet, G.; Lang, B., Proving and Applying Program Transformations Expressed with Second-Order Patterns, Acta Informatica, 11, 31-55 (1978) · Zbl 0389.68008
[31] Huet, G., The Undecidability of Unification in Third-Order Logic, Information and Control, 22, 257-267 (1973) · Zbl 0257.02038
[32] Lucchesi, C. L., The Undecidability of the Unification Problem for Third Order Languages, (Report CSRR 2059 (1972), Dept. of Applied Analysis and Computer Science, University of Waterloo)
[33] Martelli, A.; Montanari, U., An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, 4, 2, 258-282 (1982) · Zbl 0478.68093
[34] Miller, D., Proofs in Higher-Order Logic, (PhD. Dissertation (1983), Carnegie-Mellon University)
[35] Miller, D.; Nadathur, G., Higher-Order Logic Programming, (Proceedings of the Third International Conference on Logic Programming. Proceedings of the Third International Conference on Logic Programming, London (1986)) · Zbl 0900.68129
[36] Miller, D.; Nadathur, G., A Logic Programming Approach to Manipulating Formulas and Programs, (IEEE Symposium on Logic Programming. IEEE Symposium on Logic Programming, San Franciso (1987)) · Zbl 0900.68129
[37] Miller, D.; Nadathur, G., Some Uses of Higher-Order Logic in Computational Linguistics, (24th Annual Meeting of the Association for Computational Linguistics (1986)), 247-255
[38] Nadathur, G., A Higher-Order Logic as the Basis for Logic Programming, (Ph.D. Dissertation (1986), Department of Computer and Information Science, University of Pennsylvania) · Zbl 0900.68129
[39] Paulson, L. C., Natural Deduction as Higher-Order Resolution, Journal of Logic Programming, 3, 3, 237-258 (1986) · Zbl 0613.68035
[40] Pfenning, F., Proof Transformations in Higher-Order Logic, (Ph.D. thesis (1987), Department of Mathematics, Carnegie Mellon University: Department of Mathematics, Carnegie Mellon University Pittsburgh, Pa.)
[41] Pfenning, F., Partial Polymorphic Type Inference and Higher-Order Unification, (Proceedings of the 1988 ACM Conference on Lisp and Functional Programming. Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, ACM (July 1988))
[42] Pfenning, F.; Elliott, C., Higher-Order Abstract Syntax, (Proceedings of the SIGPLAN ’88 Symposium on Language Design and Implementation. Proceedings of the SIGPLAN ’88 Symposium on Language Design and Implementation, ACM (June 1988)) · Zbl 0994.68028
[43] Pietrzykowski, T., A Complete Mechanization of Second-Order Logic, JACM, 20, 2, 333-364 (1971) · Zbl 0253.68021
[44] Pietrzykowski, T.; Jensen, D., Mechanizing ω-Order Type Theory Through Unification, TCS, 3, 123-171 (1976) · Zbl 0361.02020
[45] Robinson, J. A., Mechanizing Higher-Order Logic, Machine Intelligence, 4, 151-170 (1969) · Zbl 0228.68025
[46] Snyder, W. S., Complete Sets of Transformations for General Unification, (Ph.D. Dissertation (1988), Department of Computer and Information Science, University of Pennsylvania)
[47] Statman, R., On the Existence of Closed Terms in the Typed λ-Calculus II: Transformations of Unification Problems, TCS, 15, 3, 329-338 (1981) · Zbl 0486.03011
[48] Winterstein, G., Unification in Second-Order Logic, Electronische Informationsverarbeitung und Kybernetik, 13, 399-411 (1977) · Zbl 0371.02009
[49] Zaionc, Marek, The Set of Unifiers in Typed λ-Calculus as a Regular Expression, (Proceedings of the RTA (1985)) · Zbl 0584.03010
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.