<テクニカルレポート>
Completeness of Depth-Bounded Resolution for Weakly Reducing Programs

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 SLDNF-resolution procedure is not complete with respect to the perfect model semantics for logic programs in general. In this paper, sve introduce two classes of logic programs containing function sym...bols, reducing programs and weakly reducing programs, which are characterized by the size of atom. For these classes of programs, we prove the completeness of the derivation procedure which makes use of depth-bound. First, we introduce the local finiteness of Herbrand base of a program, and prove the finite fixpoint property for the class of programs which satisfies the local finiteness. Further, we show that the class of weakly reducing programs, a subclass of locally stratified programs, has some syntactic conditions, and prove that it has the finite fixpoint property. Using the finite fixpoint property, we prove the completeness of depth-bounded derivations for weakly reducing programs. In particular, we prove the completeness of unbounded derivations for reducing programs.続きを見る

本文情報を非表示

rifis-tr-21 pdf 2.15 MB 73  

詳細

レコードID
査読有無
関連情報
注記
タイプ
登録日 2009.04.22
更新日 2017.01.20