拡張論理プログラムに対する矛盾解消アブダクションの枠組

概要

論文の詳細を見る
With the motive of establishing a contradiction-free abductive proof procedure for extended logic programs containing both explicit negations and negations as failure, we deal with a contradiction caused by complementary pairs in a model with respect to the explicit negation. Revising the usage of the exception in Kowalski and Sadri(1990), we present a way of eliminating the contradiction so that a transformation of a contradictory program can be performed to a contradiction-free program with revised exceptions. The semantics for the transformed program with revised exceptions can be defined in terms of alternating fixpoint as in Gelder(1993). Excluding incompatible complementary pairs for explicit negations, we propose an abduction framework based on 3-valued logic, where the integrity constraint is well-defined for the transformed program with revised exceptions. We find the close relationship between the satisfactory integrity constraint in the abduction framework and the semantic conditions for the transformed program. The contradiction-free abductive proof procedure is given in the propositional logic, for the satisfaction of the abduction framework constraints, where the soundness of the procedure is briefly presented.
社団法人人工知能学会の論文
2000-07-01