关键词: 析取逻辑程序, 回答集, 函数, 无基集

Abstract: Under answer sets (stable models) semantics, disjunctive logic programming with functions provides an important knowledge representation and reasoning method. As it is difficult (Σ₂-complete) to determine whether the disjunctive logic programs have an answer set, checking if a set of atoms is an answer set is coNP-complete, no effective method for computing answer sets of disjunctive logic programming with functions has been found. This paper puts forward a notion of unfounded sets for the disjunctive logic programming with functions, and finds a one-to-one relationship between the unfounded-free sets and answer sets. Accordingly this paper discovers that a model is an answer set of a logic program whenever a corresponding propositional formula is unsatisfiable. Thus, it theoretically provides an efficient approach to compute answer sets of disjunctive logic programs with functions.

Key words: disjunctive logic program, answer set, function, unfounded set