×

zbMATH — the first resource for mathematics

The undecidability of the second-order unification problem. (English) Zbl 0457.03006

MSC:
03B25 Decidability of theories and sets of sentences
03B15 Higher-order logic; type theory (MSC2010)
03D35 Undecidability and degrees of sets of sentences
03D80 Applications of computability and recursion theory
Keywords:
common instance
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Huet, G.P., The undecidability of unification in third order logic, Information and control, 22, 257-267, (1973) · Zbl 0257.02038
[2] Parikh, R., Some results on the length of proofs, Trans. amer. math. soc., 177, 29-36, (1973) · Zbl 0269.02011
[3] Paterson, M.S.; Wegman, M.N., Linear unification, J. comput. system sci., 16, 158-167, (1978) · Zbl 0371.68013
[4] Robinson, J.A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 23-41, (1965) · Zbl 0139.12303
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.