Operational semantics of resolution and productivity in Horn clause logic
Operational semantics of resolution and productivity in Horn clause logic
复制标题
Horn 子句逻辑中解析和生产力的操作语义
DOI：
10.1007/s00165-016-0403-1
复制
发表时间：
2017
影响因子：
1
通讯作者：
Fu P
中科院分区：
文献类型：
--
作者：
Fu P
本文研究了Horn子句逻辑中不同归结策略的运算性质和类型论性质。我们区分了四种不同的分辨率：统一分辨率（SLD分辨率），术语匹配分辨率，最近引入的结构分辨率和部分（或懒惰）分辨率。我们把它们统一表示为抽象的归约系统，这使我们能够对它们的性质进行彻底的比较分析。为了匹配这种小步骤语义，我们建议采用霍华德的SystemHas的类型理论语义对应物。使用SystemH，我们将Horn公式解释为类型，并将给定公式的推导解释为居住在该公式给出的类型中的证明项。我们证明了这些抽象约简系统相对于SystemH的合理性，并证明了SLD-分辨率和结构分辨率相对于SystemH的完备性。我们确定的条件下，结构分辨率在操作上相当于SLD分辨率。我们展示了没有存在变量的Horn子句程序的术语匹配解决方案与术语重写之间的对应关系。
This paper presents a study of operational and type-theoretic properties of different resolution strategies in Horn clause logic. We distinguish four different kinds of resolution: resolution by unification (SLD-resolution), resolution by term-matching, the recently introduced structural resolution, and partial (or lazy) resolution. We express them all uniformly as abstract reduction systems, which allows us to undertake a thorough comparative analysis of their properties. To match this small-step semantics, we propose to take Howard’s SystemHas a type-theoretic semantic counterpart. Using SystemH, we interpret Horn formulas as types, and a derivation for a given formula as the proof term inhabiting the type given by the formula. We prove soundness of these abstract reduction systems relative to SystemH, and we show completeness of SLD-resolution and structural resolution relative to SystemH. We identify conditions under which structural resolution is operationally equivalent to SLD-resolution. We show correspondence between term-matching resolution for Horn clause programs without existential variables and term rewriting.
登录
查看更多内容
证明相关的核心递归解析
DOI：
--
发表时间：
2015
期刊：
Fuji International Symposium on Functional and Logic Programming
影响因子：
--
作者：
Peng Fu;Ekaterina Komendantskaya;Tom Schrijvers;Andrew Pond
通讯作者：
Andrew Pond
结构解析：霍恩子句逻辑中的共归纳证明搜索和证明构造的框架
DOI：
--
发表时间：
2015
期刊：
arXiv.org
影响因子：
--
作者：
Ekaterina Komendantskaya;Patricia Johann
通讯作者：
Patricia Johann
类型类：设计空间的探索
DOI：
--
发表时间：
1997
期刊：
影响因子：
--
作者：
S. Jones;Mark P. Jones;E. Meijer
通讯作者：
E. Meijer
在逻辑框架中机械化元理论
影响因子：
1.1
作者：
R. Harper;Daniel R. Licata
通讯作者：
Daniel R. Licata
影响因子：
0.7
作者：
Komendantskaya E
通讯作者：
Komendantskaya E