Non-Monotonic Reasoning · 2004 · 35 citations · 8 references
Open access
Applied LogicEngineeringVerificationWell-founded SemanticsMajor SemanticsDisjunctive ProgrammingHigher-order LogicFormal VerificationLogic ProgrammingNon-classical LogicMonotone AggregatesComputer ScienceMonotone Aggregate AtomsOperator-based ApproachProgram AnalysisAutomated ReasoningPropositional LogicLogical FrameworkFormal MethodsFirst-order LogicNormal Logic ProgramsDisjunctive Programs
Existing semantics for normal logic programs and those with aggregates are defined as fixpoints of the one‑step provability operator, yet no systematic operator‑based semantics has been developed for disjunctive logic programs. The paper initiates a systematic operator‑based approach to the semantics of disjunctive logic programs. We define non‑deterministic one‑step‑provability operators on the lattice of interpretations and use them to characterize models, minimal models, supported models, and stable models of disjunctive logic programs, extending the framework to four‑valued semantics and propositional programs with monotone aggregates. Our algebraic concepts, results, and proof techniques indicate that the framework can be generalized to abstract algebraic settings of non‑deterministic operators on complete lattices.
All major semantics of normal logic programs and normal logic programs with aggregates can be described as fixpoints of the one-step provability operator or of operators that can be derived from it. No such systematic operator-based approach to semantics of disjunctive logic programs has been developed so far. This paper is the first step in this direction. We formalize the concept of one-step-provability for disjunctive logic programs by means of non-deterministic operators on the lattice of interpretations. We establish characterizations of models, minimal models, supported models and stable models of disjunctive logic programs in terms of pre-fixpoints and fixpoints of non-deterministic immediateconsequence operators and their extensions to the four-valued setting. We develop our results for programs in propositional language extended with monotone aggregate atoms. For the most part, our concepts, results and proof techniques are algebraic, which opens a possibility for further generalizations to the abstract algebraic setting of non-deterministic operators on complete lattices.
8