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

作成者
本文言語
出版者
発行日
収録物名
出版タイプ
アクセス権
関連DOI
関連URI
関連情報
概要 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.続きを見る

本文ファイル

pdf rifis-tr-21 pdf 2.15 MB 416  

詳細

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

この資料を見た人はこんな資料も見ています