A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
复制标题
逻辑编程的证明理论方法。
DOI：
--
复制
发表时间：
1990
影响因子：
0.7
通讯作者：
P. Schroeder
中科院分区：
文献类型：
--
作者：
Lars Hallnäs;P. Schroeder
在本文中，明确霍恩子句程序的证明理论框架内进行了调查，程序条款被认为是一个正式的系统规则。在此基础上，通过纯证明论方法，证明了SLD-分解的可靠性和完备性。扩展Horn子句被定义为更高层次的规则，并与基于子句体中蕴涵公式的方法相关。在本系列第二部分讨论的进一步扩展中，程序子句被看作是原子归纳定义中的子句，证明了一个额外的推理模式：一个反射原则，大致对应于将程序子句解释为自然演绎意义上的引入规则。查询的评估程序相对于确定霍恩子句程序的定义扩展是健全和完整的。具有一般消除模式的微积分甚至允许
In this paper definite Horn clause programs are investigated within a proof-theoreti c framework; program clauses being considered rules of a formal system. Based on this approach, the soundness and completeness of SLD-resolutio n is established by purely proof-theoretic methods. Extended Horn clauses are defined as rules of higher levels and related to an approach based on implication formulae in the bodies of clauses. In a further extension, which is treated in Part II of this series, program clauses are viewed as clauses in inductive definitions of atoms, justifying an additional inference schema: a reflection principle that roughly corresponds to interpreting the program clauses as introduction rules in the sense of natural deduction. The evaluation procedures for queries with respect to the defined extensions of definite Horn clause programs are shown to be sound and complete. The sequent calculus with the general elimination schema even permits the