综述:一般逻辑程序的证明论语义

Survey: Proof Theory Semantics of General Logic Program

一般逻辑程序是知识表示的重要工具,也是非单调推理研究的领域之一。一般逻辑程序的证明论语义给出一个证明过程,对应于相应的模型论语义,同时也为模型论语义的实现提供基础。本文对一般逻辑程序的证明论研究进行综述,涉及到基于各种模型论语义的证明过程,并且对各研究在语法约束、推理方式、正确性和完备性结论及实现的情况等各方面加以比较,最后给出了此问题进一步的一些研完方向。

General logic programming is an important knowledge representation tool,and is an area of nonmonotonic reasoning. Proof theory semantics provides a proof procedure, corresponds to model theory semantics, which may lead to the implementation of model theory semantics. A survey is given for research on proof theory of general logic program. Proof procedures on different kinds of model theories are discussed. The comparison is given about syntax limitation, evaluation methods, soundness and completeness, as well as implementation. Also, some areas for advanced research are discussed.