A higher-order logic as the basis for logic programming
A higher-order logic as the basis for logic programming
复制标题
高阶逻辑作为逻辑编程的基础
DOI：
--
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
G. Nadathur
中科院分区：
文献类型：
--
作者：
G. Nadathur
本论文的目的是为逻辑程序设计范式中的高阶特征提供一个形式化的基础。为了达到这个目的，高阶逻辑的一种非外延形式，它是基于丘奇的简单类型理论，用来提供一阶逻辑的定分句的概括。具体地说，一类被称为高阶定语句的公式进行了描述。这些公式通过将一阶项替换为类型化$\lambda$ -演算的项，并通过提供对谓词和函数变量的量化来扩展定语句。结果表明，这些公式，连同概念的证明，在高阶逻辑，提供了一个抽象的描述计算是类似于一阶的情况下。虽然在高阶逻辑中的证明的建设往往是复杂的任务，找到适当的替代谓词变量，它表明，必要的替代谓词变量可以严格限制在高阶定语句的上下文中。这一观察使一个完整的定理证明这些公式的过程的描述。该程序构造证明基本上是通过交织高阶统一与backchaining的含义，并构成了一个概括，高阶上下文中，众所周知的SLD决议程序的确定条款。这些调查的结果被用来描述逻辑编程语言称为$\lambda$ Prolog。这种语言包含了Prolog等语言的所有特征，此外，还拥有某些高阶特征。这些额外的功能的性质进行说明，它是如何使用的条款（类型）$\lambda$ -演算作为数据结构提供了丰富的逻辑编程范式的来源。
The objective of this thesis is to provide a formal basis for higher-order features in the paradigm of logic programming. Towards this end, a non-extensional form of higher-order logic that is based on Church''s simple theory of types is used to provide a generalisation to the definite clauses of first-order logic. Specifically, a class of formulas that are called higher-order definite sentences is described. These formulas extend definite clauses by replacing first-order terms by the terms of a typed $\lambda$ -calculus and by providing for quantification over predicate and function variables. It is shown that these formulas, together with the notion of a proof in the higher-order logic, provide an abstract description of computation that is akin to the one in the first-order case. While the construction of a proof in a higher-order logic is often complicated by the task of finding appropriate substitutions for predicate variables, it is shown that the necessary substitutions for predicate variables can be tightly constrained in the context of higher-order definite sentences. This observation enables the description of a complete theorem-proving procedure for these formulas. The procedure constructs proofs essentially by interweaving higher-order unification with backchaining on implication, and constitutes a generalisation, to the higher-order context, of the well-known SLD-resolution procedure for definite clauses. The results of these investigations are used to describe a logic programming language called $\lambda$ Prolog. This language contains all the features of a language such a Prolog, and, in addition, possesses certain higher-order features. The nature of these additional features is illustrated, and it is shown how the use of the terms of a (typed) $\lambda$ -calculus as data structures provides a source of richness to the logic programming paradigm.