Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
复制标题
结构解析：霍恩子句逻辑中的共归纳证明搜索和证明构造的框架
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Patricia Johann
中科院分区：
文献类型：
--
作者：
Ekaterina Komendantskaya;Patricia Johann
逻辑编程（英语：Logic programming，LP）是一种基于一阶Horn子句逻辑的编程语言，它使用SLD-归结作为半决策过程。有限的SLD计算是归纳的声音和完整的最少Herbrand模型的逻辑程序。对偶地，SLD分解的共递归方法将无限SLD计算视为连续逼近程序的最大完全Herbrand模型中包含的无限项。在LP中实现协递归的最新算法基于循环检测。然而，这样的算法只支持推理的逻辑蕴涵合理的条款，他们没有考虑到生产力的重要性质，在无限的SLD计算。因此，循环检测落后于交互式定理证明（ITP）和项重写系统（TRS）中的共归纳方法。
结构分解是一种新提出的替代SLD分解的方法，它可以定义和半决定一个适合于LP的生产力概念。在本文中，我们证明了健全的结构分辨率相对于Herbrand模型语义生产归纳，共归纳，混合归纳共归纳逻辑程序。
我们介绍了两个算法，支持共归纳证明搜索无限生产条件。一个算法结合了循环检测的方法与生产性结构的解决方案，从而保证生产力的共归纳证明的无穷有理项。另一种则允许对无限非理性生产性术语的片段进行懒惰的合理观察。这使得LP中的共归纳方法与ITP和TRS中基于生产力的共归纳观察方法相提并论。
Logic programming (LP) is a programming language based on first-order Horn clause logic that uses SLD-resolution as a semi-decision procedure. Finite SLD-computations are inductively sound and complete with respect to least Herbrand models of logic programs. Dually, the corecursive approach to SLD-resolution views infinite SLD-computations as successively approximating infinite terms contained in programs' greatest complete Herbrand models. State-of-the-art algorithms implementing corecursion in LP are based on loop detection. However, such algorithms support inference of logical entailment only for rational terms, and they do not account for the important property of productivity in infinite SLD-computations. Loop detection thus lags behind coinductive methods in interactive theorem proving (ITP) and term-rewriting systems (TRS).
Structural resolution is a newly proposed alternative to SLD-resolution that makes it possible to define and semi-decide a notion of productivity appropriate to LP. In this paper, we prove soundness of structural resolution relative to Herbrand model semantics for productive inductive, coinductive, and mixed inductive-coinductive logic programs.
We introduce two algorithms that support coinductive proof search for infinite productive terms. One algorithm combines the method of loop detection with productive structural resolution, thus guaranteeing productivity of coinductive proofs for infinite rational terms. The other allows to make lazy sound observations of fragments of infinite irrational productive terms. This puts coinductive methods in LP on par with productivity-based observational approaches to coinduction in ITP and TRS.
登录
查看更多内容
Horn 子句逻辑中解析和生产力的操作语义
影响因子：
1
作者：
Fu P
通讯作者：
Fu P
影响因子：
0.7
作者：
Komendantskaya E
通讯作者：
Komendantskaya E
具有保护递归的高效协同编程
影响因子：
--
作者：
Atkey R
通讯作者：
Atkey R
Coq 中核心递归函数的归纳和共归纳成分
影响因子：
--
作者：
Bertot Y
通讯作者：
Bertot Y