证明一般逻辑程序终止性的实用方法

E. Marchiori

证明一般逻辑程序终止性的实用方法

人工智能 2014-11-17 v1

作者: E. Marchiori

摘要

带有否定体原子的逻辑程序（此处称为一般逻辑程序）的终止性是一个重要课题。原因之一在于，许多用于处理否定原子的计算机制，如 Clark 的失败即否定（negation as failure）和 Chan 的构造性否定，都基于终止条件。本文介绍了一种针对 Prolog 选择规则证明一般逻辑程序终止性的方法论。其思想是区分程序中终止是否依赖于选择规则的部分。为此，引入了低可接受、弱向上可接受和向上可接受程序的概念。我们利用这些概念发展了一种证明一般逻辑程序终止性的方法论，并展示了非单调推理中有趣的问题如何形式化并通过终止的一般逻辑程序来实现。

关键词

一般逻辑程序终止性分析 Prolog 选择规则非单调推理失败即否定可接受程序

引用

@article{arxiv.cs/9604102,
  title  = {Practical Methods for Proving Termination of General Logic Programs},
  author = {E. Marchiori},
  journal= {arXiv preprint arXiv:cs/9604102},
  year   = {2014}
}

备注

See http://www.jair.org/ for any accompanying files

证明一般逻辑程序终止性的实用方法

摘要

关键词

引用

备注

相关论文