霍恩子句逻辑中归结与生成性的操作语义
计算机科学中的逻辑
2016-10-31 v2
摘要
本文提出对霍恩子句逻辑中不同归结策略的操作与类型论性质的研究。我们区分四种不同的归结：基于合一的归结（SLD-归结）、基于项匹配的归结、近期引入的结构归结以及部分（或惰性）归结。我们将它们统一表达为抽象归约系统，从而能够对它们的性质进行彻底的比较分析。为匹配这种小步语义，我们提议采用霍华德（Howard）的 System H 作为类型论语义对应物。利用 System H，我们将霍恩公式解释为类型，并将给定公式的推导解释为居于该公式所给类型的证明项。我们证明了这些抽象归约系统相对于 System H 的可靠性，并展示了 SLD-归结和结构归结相对于 System H 的完备性。我们确定了结构归结在操作上等价于 SLD-归结的条件。我们展示了无存在变量霍恩子句程序的项匹配归结与项重写之间的对应关系。
引用
@article{arxiv.1604.04114,
title = {Operational Semantics of Resolution and Productivity in Horn Clause Logic},
author = {Peng Fu and Ekaterina Komendantskaya},
journal= {arXiv preprint arXiv:1604.04114},
year = {2016}
}
备注
Journal Formal Aspect of Computing, 2016