## 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

ETPS
Full Text:

### 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., () [5] Barendregt, H.P., () [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, () [9] Elliot, C., Higher-order unification with dependent function types, () [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, () [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). · Zbl 0731.03005 [14] Farmer, W., “A Unification-Theoretic Method for Investigating the k-Provability Problem,” submitted for publication. · Zbl 0735.03001 [15] Felty, A.; Miller, D., Specifying theorem provers in a higher-order logic programming language, () · Zbl 0645.68097 [16] Gallier, J.H., () [17] Gallier, J.H.; Snyder, W., A general complete E-unification procedure, (1987), 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, () [21] 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, () [24] Hannan, J.; Miller, D., Uses of higher-order unification for implementing program transformers, () [25] Herbrand, J., “Sur la Théorie de la Démonstration,” in: Logical Writings, W. Goldfarb, ed., Cambridge, 1971. [26] Hindley, J.; Seldin, J., () [27] Huet, G., A mechanization of type theory, (), 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,…,ω, () [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, () [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, () [35] Miller, D.; Nadathur, G., Higher-order logic programming, () · Zbl 0900.68129 [36] Miller, D.; Nadathur, G., A logic programming approach to manipulating formulas and programs, () · Zbl 0900.68129 [37] Miller, D.; Nadathur, G., Some uses of higher-order logic in computational linguistics, (), 247-255 [38] Nadathur, G., A higher-order logic as the basis for logic programming, () · 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, () [41] Pfenning, F., Partial polymorphic type inference and higher-order unification, () [42] Pfenning, F.; Elliott, C., Higher-order abstract syntax, () · 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, () [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, () · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.