A Complete Mechanization of Second-Order Type Theory

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Complete Mechanization of Second-Order Type Theory

Full text

Pdf (2.04 MB)

Source

Journal of the ACM (JACM) archive
Volume 20 , Issue 2 (April 1973) table of contents

Pages: 333 - 364

Year of Publication: 1973

ISSN:0004-5411

Author

Tomasz Pietrzykowski

Department of Applied Analysis and Computer Science, University of Waterloo, Waterloo, Ontario, Canada

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 31, Citation Count: 5

Additional Information:

abstract 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/321752.321764 What is a DOI?

ABSTRACT

A generalization of the resolution method for higher order logic is presented. The languages acceptable for the method are phrased in a theory of types of order w (all finite types)—including the &lgr;-operator, propositional functors, and quantifiers. The resolution method is, of course, a machine-oriented theorem search procedure based on refutation. In order to make this method suitable for higher order logic, it was necessary to overcome two sorts of difficulties. The first is that the unifying substitution procedure—an essential feature of the classic first-order resolution—must be generalized (it is noted that for the higher order unification the proper notion of substitution will include &lgr;-normalization). A general unification algorithm is produced and proved to be complete for second-order languages. The second difficulty arises because in higher order languages, semantic intent is essentially more “interwoven” in formulas than in first-order languages. Whereas quantifiers could be eliminated immediately in first-order resolution, their elimination must be deferred in the higher order case. The generalized resolution procedure which the author produces thus incorporates quantifier elimination along with the familiar features of unification and tautological reduction. It is established that the author's generalized resolution procedure is complete with respect to a natural notion of validity based on Henkin's general validity for type theory. Finally, there are presented examples of the application of the method to number theory and set theory.

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	ANDREWS, P. Resolution in type theory. J. Symbolic Logic $6, 3 (1971), 414-432.
	2	BLEDSOE, W.W. Splitting and reduction heuristics in automatic theorem proving. Artificial Intelligence ~ (1971), pp. 57-78.
	3	VE BRUIJN, N.G. The mathematical language AUTOMATH, its usage and some of its extensions. Symposium on Automatic Demonstration, Versailles, Dec. 1968, Springer- Verlag, 1970, pp. 29-61.
	4	CHURCH, A. The Calculi of Lambda-Conversion. Princeton U. Press, Princeton, N. J., 1941.
	5	DARLXNGTON, J.L. Automatic theorem proving with equality substitutions and mathematical induction. In Machine Intelligence 3, D. Michie (Ed.), American Elsevier, New York, 1968, pp. 113-130.
	6	DARLINGTON, J.L. A partial mechanization of second-order logic. In Machine Intelligence 6, B. Melzer and D. Michie (eds.), American Elsevier, New York, 1971, pp. 91-100.
	7	GOULD, W.E. A matching procedure for omega-order logic. Ph.D. thesis, Princeton U., Princeton, N. J.; University Microfilms, Ann Arbor, Mich.
	8	HENKIN, L. Completeness in the theory of types. J. Symbolic Logic 15 (1960), 81-91.
	9	JENSEN, D. C. A two-valued type theory model convenient for resolution theoremproving. CSRR 2055, Dep. of Applied Analysis and Comput. Sci., U. of Waterloo, Waterloo, Ont., Canada, 1971.
	10	MELTZER, B. Power amplification for theorem-provers. In Machine Intelligence 5, B. Meltzer and D. Michie (Eds.), American Elsevier, New York, 1970, pp. 165-180.
	11	MONK, J. D. Introduction to Set Theory. McGraw-Hill, New York, 1969.
	12	PIETaZYKOWSKI, T. A natural language for formal mathematical reasoning (TPL 2), Part I. CSRR 2015, Dep. of Applied Analysis and Comput. Sci., U. of Waterloo, Waterloo, Ont., Canada, 1970.
	13	PIETRZYKOWSKI, T. A complete mechanization of second order skolemized logic. CSRR 2036, Dep. of Applied Analysis and Comput. Sci., U. of Waterloo, Waterloo, Ont., Canada, 1971.
	14	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]
	15	ROBINSON, J.A. New directions in mechanical theorem proving. Proe. IFIP Cong. 68, Vol. 1, North-Holland Pub. Co., Amsterdam, pp. 63-67.
	16	ROmNSON, J.A. Mechanizing higher-order logic. In Machine intelligence ~, B. Meltzer and D. Michie (Eds.), American Elsevier, New York, 1969, pp. 157-172.
	17	SHOENFIEm), J. R. Mathematical Logic, Addison-Wesley, Reading, Mass., 1967.

CITED BY 5

	Kevin Knight, Unification: a multidisciplinary survey, ACM Computing Surveys (CSUR), v.21 n.1, p.93-124, March 1989
	Peter B. Andrews, Classical type theory, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Fujio Nishida , Shinobu Takamatsu , Yoneharu Fujita , Tadaaki Tani, Semi-Automatic Program Construction from Specifications Using Library Modules, IEEE Transactions on Software Engineering, v.17 n.9, p.853-871, September 1991
	W. W. Bledsoe, Set variables, Proceedings of the 5th international joint conference on Artificial intelligence, p.501-510, August 22-25, 1977, Cambridge, USA
	Gerard P. Hubt, A mechanization of type theory, Proceedings of the 3rd international joint conference on Artificial intelligence, p.139-146, August 20-23, 1973, Stanford, USA