A Complete Mechanization of Second-Order Type Theory
A Complete Mechanization of Second-Order Type Theory
复制标题
二阶类型理论的完整机械化
DOI：
10.1145/321752.321764
复制
发表时间：
1973
期刊：
影响因子：
--
通讯作者：
T. Pietrzykowski
中科院分区：
文献类型：
--
作者：
T. Pietrzykowski
本文给出高阶逻辑归结方法的一个推广。该方法所能接受的语言都是以w阶类型（所有有限类型）的理论来表述的，包括λ-算子、命题函子和量词。当然，归结方法是一种基于反驳的面向机器的定理搜索过程。为了使这种方法适用于高阶逻辑，必须克服两类困难。第一个是统一替换过程-经典一阶分解的一个基本特征-必须被推广（注意，对于高阶统一，替换的正确概念将包括λ-归一化）。给出了二阶语言的统一算法，并证明了该算法的完备性。第二个困难是因为在高阶语言中，语义意图在公式中比在一阶语言中更“交织”。虽然量词可以立即消除在一阶分辨率，他们的消除必须推迟在高阶的情况下。因此，作者所产生的广义归结过程结合了量词消除沿着以及统一和重言式归约的熟悉特征。它是建立在Henkin的一般有效性的类型论的基础上，作者的广义决议程序是完整的一个自然的概念的有效性。最后，给出了该方法在数论和集合论中的应用实例。
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 λ-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 λ-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.