Assumption Sets for Extended Logic Programs

Thomas Eiter^{∗}, Nicola Leone^{†}and David Pearce^{‡}

Abstract

Generalising the ideas of [10] we define a simple extension of the notion of unfounded set, called assumption set, that applies to disjunctive logic programs with strong negation. We show that assumption-free interpretations of such extended logic programs coincide with equilibrium models in the sense of [13] and hence with the answer sets of [3, 4].

Contents

1 Introduction 2 2 Assumption Sets 2 3 Logical Preliminaries 3 4 N2 and Assumption Sets 4 5 Equilibrium Logic 5

∗Information Systems Dept, Technical University of Vienna, A-1040 Vienna, e-mail :

eiter@kr.tuwien.ac.at

†Information Systems Dept, Technical University of Vienna, A-1040 Vienna, e-mail:

leone@dbai.tuwien.ac.at

‡DFKI GmbH, PF 15 11 50, D-66041 Saarbrücken, e-mail: David.Pearce@dfki.de

1 Introduction

The notion of unfounded set for normal logic progams was introduced in [2]. It was extended to disjunctive logic programs in [10] where it was used to give declarative characterisations of stable models for disjunctive programs (see also [9]). In this note we show that a simple generalisation of the concept of unfounded set can be used to capture answer sets for disjunctive programs extended with an additional strong negation operator([3, 4]). Instead of unfounded set, we speak here of assumption set. To prove the equivalence with answer sets we use the characterisation of answer sets given by the third author in [13].

2 Assumption Sets

We deal with disjunctive ground logic programs extended by an additional negation, called strong negation. The usual default or weak negation will be denoted by ’¬’, strong negation will be denoted by ’∼’. A literal is an atom or strongly negated atom. A logic program is a set of formulas φ, also called rules, of the form:

L_{1} ∧ … ∧ L_{m} ∧ ¬L_{m+1} ∧ … ∧ ¬L_{n} → K_{1} ∨ … ∨ K_{k}  (1)

where the L_{i} and K_{j} are literals. The consequent K_{1} ∨ … ∨ K_{k} of a formula φ of form (1) is called the head and denoted by h(φ). The antecedent L_{1} ∧ … ∧ L_{m} ∧ ¬L_{m+1} ∧ … ¬ ∧ L_{n} is called the body and denoted by b(φ). We distinguish between the weakly positive part of the body, denoted by b^{+}(φ), being L_{1} ∧ … ∧ L_{m} and the weakly negative part, b^{−}(φ), which is ¬L_{m+1} ∧ … ∧ ¬L_{n}.

In order to define assumption sets in this more general setting, we need to consider interpretations comprising sets of literals. Accordingly we say that an interpretation I is a non-empty and consistent set of literals, ie. for no atom A do we have both A ∈ I and ∼ A ∈ I. Truth and falsity wrt interpretations is defined as follows. A literal L is true wrt I, in symbols I ⊧ L if L ∈ I, and false (I |̸= L) otherwise. The ⊧ relation is extended as follows. I ⊧ ¬L if I |̸= L, equivalently L ∉ I. It follows from the consistency condition that I ⊧∼ A implies I ⊧ ¬A. I ⊧ φ ∧ ψ if I ⊧ φ and I ⊧ ψ. I ⊧ φ ∨ ψ if I ⊧ φ or I ⊧ ψ. I ⊧ φ → ψ if I ⊧ ψ whenever I ⊧ φ. An interpretation I is a model of a program Π if I ⊧ φ for each formula φ ∈ Π.

With respect to this more general notion of interpretation, we can define the concept of assumption set as a simple extension of the usual notion of unfounded set (it reduces to the ordinary notion of unfounded set of [2] in the case of total interpretations on normal logic programs without disjunction and strong negation).

Definition 1 Let Π be a logic program and I an interpretation for Π. A nonempty subset X of I is said to be an assumption set for Π wrt I if for each L ∈ X, every formula φ of Π having L in its head satisfies at least one of the following three conditions.

1. The weakly negative body is false wrt I, ie. I |̸= b^{−}(φ).

2. The weakly positive body is false wrt I\X, ie. I\X |̸= b^{+}(φ).

3. The head is true wrt I\X, ie. I\X ⊧ h(φ).

Given a program Π, an interpretation I is said to be assumption-free if there are no assumption sets for Π wrt I.

Models of a program that are assumption-free correspond to the answer sets of the program. To show this we use a characterisation of answer sets as minimal models of a certain kind in the logic of here-and-there with strong negation, denoted by N2. The minimal models in question were studied in [13] and are called equilibrium models. We show that for disjunctive programs equilibrium models and assumption-free models coincide.^{1} In fact we shall demonstrate an even closer link between assumption sets and N2-models, to be described in the next section.

3 Logical Preliminaries

In logic, the notion of strong negation was introduced by Nelson [12] in 1949. Nelson’s logic N is known as constructive logic with strong negation. N can be regarded as an extension of intuitionistic logic, H, in which the language of intuitionistic logic is extended by adding a new, strong negation symbol, ‘∼’, with the intepretation that ∼ A is true if A is constructively false. The axioms and rules of N are those of H (see eg. [1]) together with the axiom schemata involving strong negation, originally given by Vorob’ev [15, 16] (see [13]). A Kripke-style semantics for N is straightforward. In general, one may take Kripke-frames for intuitionistic logic, but require valuations V to be partial rather than total, extending the truth-conditions to include the strongly negated formulas (see eg. [6, 1]). Since we deal here with fully instantiated or ground logic programs we omit the semantics of quantification. Accordingly, for our present purposes we consider Kripke frames F, where

F = ⟨W, ≤⟩

such that W is a set of stages or possible worlds and ≤ is a partial-ordering on W. A Nelson-model M is then defined to be a frame F together with an N-valuation V assigning 1, 0 or −1 to each sentence φ and world w ∈ W. Moreover, V satisfies the following. If A is an atom, then if V (w, A) ≠ 0 then V (w′, A) = V (w, A) for all w′ such that w ≤ w′. In addition,

V (w, ∼ φ) = −V (w, φ)
V (w, φ ∨ ψ) = max{V (w, φ), V (w, ψ)}
V (w, φ ∧ ψ) = min{V (w, φ), V (w, ψ)}

V (w, φ → ψ) = \{ \begin{matrix}1 & iff for all w′ ≥ w, V (w′, φ) = 1 implies V (w′, ψ) = 1 \\ −1 & iff V (w, φ) = 1 and V (w, ψ) = −1 \end{matrix}

1Equilbrium models remain more general since they are defined for syntactically broader classes of theories.

V (w, ¬φ) = 1 ⇔ V (w′, φ) < 1 for all w′ ≥ w
V (w, ¬φ) = −1 ⇔ V (w, φ) = 1

A sentence φ is said to be true in a Nelson-model M, written M ⊧_{N} φ, if for all w ∈ W, V (w, φ) = 1. Similarly, M is said to be an N-model of a set Π of N-sentences, if M ⊧_{N} φ, for all φ ∈ Π.

We also consider intermediate logics, obtained by adding additional axioms to H. An intermediate logic is called proper if it is contained in classical logic. For any intermediate logic Int, we can define a least constructive (strong negation) extension of Int, obtained simply by adding to Int the Vorob’ev axioms. In the lattice of intermediate logics, classical logic has a unique lower cover which is the supremum of all proper intermediate logics. This greatest proper intermediate logic will be denoted by J. It is often referred to as the logic of “here-and-there”, since it is characterised by linear Kripke frames having precisely two elements or worlds: ‘here’ and ‘there’. J is also characterised by the three element Heyting algebra, and is known by a variety of other names, including the Smetanich logic, and the 3-valued logic of Gödel, [5]. Łukasiewicz [11] characterised J by adding to H the axiom schema

(¬α → β) → (((β → α) → β) → β).

Let us denote by N2 the least constructive extension of J, which is complete for the above class of 2-element, here-and-there frames under 3-valued, Nelson valuations (see [8]).

4 N2 and Assumption Sets

Since N2 is the logic determined by Nelson models based on the 2-element, ‘here-and-there’ frame, an N2-model N is a structure ⟨{h, t}, ≤, V ⟩, where the worlds h and t are reflexive, and h ≤ t. Simplifying, we can also regard an N2-model simply as a pair ⟨H, T ⟩, where H is the set of literals verified at world h and T is the set of literal verified at world t. Note that for any such model ⟨H, T ⟩, we always have H ⊆ T. We now consider the relation between assumption sets and N2-models.

Proposition 1 Let Π be a program and let M be an interpretation such that M ⊧ Π. A non-empty subset X of M is an assumption-set for Π wrt M iff ⟨M\X, M⟩ is an N2-model of Π.

Proof. Let M be an interpretation such that M ⊧ Π. Consider a non-empty subset X of M such that X is an assumption set for Π wrt M. We show that ⟨M\X, M⟩ is an N2-model of Π. Consider the conditions 1-3 of Definition 1 applied to X, and consider any formula φ of Π whose head contains some literal in X. If condition 1 holds, then, since M ⊧ φ, clearly φ holds at each point in ⟨M\X, M⟩, by the semantics for N2; so ⟨M\X, M⟩ ⊧ φ. Likewise it is easily seen that φ is verified at the first point if either 2 or 3 holds; and it is automatically verified at the second point, since M is a model of the program.

It remains to consider those formulas φ of Π whose heads contain no literals in X. For such a formula φ of form (1), since M ⊧ φ, the following condition is satisfied:

L_{1}, …, L_{m} ∈ M & L_{m+1}, …, L_{n} ∉ M ⇒ K_{i} ∈ M for some i ≤ k (2)

It follows that if L_{1}, …, L_{m} ∈ M\X and L_{m+1}, …, L_{n} ∉ M, then K_{i} ∈ M for some i ≤ k, hence K_{i} ∈ M\X, since no K_{i} is in X. Given that φ is already satisfied in M, this is precisely the condition for φ to be verified also at the first point in ⟨M\X, M⟩. So ⟨M\X, M⟩ ⊧_{N2} Π, as required.

For the other direction, suppose that M = ⟨M′, M⟩ is an N2-model of Π with M′ a proper subset of M. We verify that M\M′ is an assumption set for Π wrt M. Set X = M\M′ and consider any formula φ of Π whose head contains a literal in X. Since M ⊧ φ, in particular wrt the first point M′, either h(φ) is true or b(φ) is false. The latter condition occurs if either b^{+}(φ) is false wrt to M′ or if b^{−}(φ) is false wrt M. So at least one of conditions 1 - 3 of Definition 1 holds for X. Therefore X is an assumption-set for Π wrt M, as required. □

5 Equilibrium Logic

Equilibrium logic was introduced in [13, 14] as a special kind of minimal model reasoning in N2, defined as follows.

Definition 2 We define a partial ordering ≤ among N2-models as follows. For any models M = ⟨H, T ⟩, M′ = ⟨H′, T′⟩, we set M ≤ M′ iff T = T′ and H ⊆ H′. A model M of a program Π is said to be a minimal model of Π, if it is minimal under the ≤-ordering among all models of Π.

Definition 3 An N2-model ⟨H, T ⟩ of Π is said to be an equilibrium model of Π iff it is minimal and H = T.

Thus an equilibrium model is a model ⟨H, T ⟩ in which H = T and no other model verifying the same literals at its t-world verifies fewer literals at its hworld. Clearly this model is equivalent to a one-element model. The system of inference based on reasoning from all equilibrium models of a theory is called equilibrium logic. We now state the equivalence between assumption-free sets, equilibrium models and answer sets ([3, 4]).

Proposition 2 Let Π be a program and let M be an interpretation such that M ⊧ Π. The following three conditions are equivalent.

1. M is assumption-free for Π

2. M is an answer set of Π

3. ⟨M, M⟩ is an equilibrium model of Π

Proof. The equivalence of 2 and 3 was shown in [13]. The equivalence of 1 and 3 is a simple corollary of Proposition 1. If M is a model of Π that is not assumption-free, then there exist a non-empty assumption-set X wrt M.

By Proposition 1, ⟨M\X, M⟩ is an N2-model of Π, and so ⟨M, M⟩ is not in equilibrium. Conversely, if ⟨M, M⟩ is not in equilibrium, then there exist an N2-model ⟨M′, M⟩ of Π, where M′ is a proper subset of M. By Proposition 1, M\M′ is an assumption-set for Π wrt M. Hence M is not assumption-free. □

References

[1] van Dalen, D, Intuitionistic Logic, in D Gabbay, & F Guenthner (eds), Handbook of Philosophical Logic, Vol. III, Kluwer, Dordrecht, 1986.

[2] Van Gelder, A, Ross, K A, & Schlipf, J S, The Well-Founded Semantics for General Logic Programs, J Assoc Comput Mach 38 (1991), 620-650.

[3] Gelfond, M & Lifschitz, V, Logic Programs with Classical Negation, in D Warren & P Szeredi (eds), Proc ICLP-90, MIT Press, 1990, 579– 597.

[4] Gelfond, M, & Lifschitz, V, Classical Negation in Logic Programs and Disjunctive Databases, New Generation Computing (1991), 365-387.

[5] Gödel, K, Zum intuitionistischen Aussagenkalkül, Anzeiger der Akademie der Wissenschaften in Wien 69 65-66; reprinted in em Kurt Gödel, Collected Works, Volume 1, OUP, 1986.

[6] Gurevich, Y, Intuitionistic Logic with Strong Negation, Studia Logica 36 (1977), 49-59.

[7] Heyting, A, Die formalen Regeln der intuitionistischen Logik, Sitz. Berlin 1930, 42-56.

[8] Kracht, M, On Extensions of Intermediate Logics by Strong Negation, Journal of Philosophical Logic 27 (1998), 49-73.

[9] Leone, N, Rullo, P, & Scarcello, F, Declarative and Fixpoint Characterizations of Disjunctive Stable Models, in J Lloyd (ed), Proc ILPS ’95, MIT Press, 1995.

[10] Leone, N, Rullo, P & Scarcello, F, Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics, and Computation, Information and Computation 135 (1997), 69-112.

[11] Łukasiewicz, J, Die Logik und das Grundlagenproblem, in Les Entretiens de Zurich sur les Fondaments et la Methode des Sciences Mathematiques 1938, Zurich, 1941.

[12] Nelson, D, Constructible Falsity, JSL 14 (1949), 16–26.

[13] Pearce, D, A New Logical Characterisation of Stable Models and Answer Sets, in J Dix, L M Pereira & T Przymusinski (eds), Non-Monotonic Extensions of Logic Programming. Proc NMELP 96, LNAI 1216, Springer, 1997.

[14] Pearce, D, From Here to There: Stable Negation in Logic Programming, in D Gabbay & H Wansing (eds), What is Negation?, Kluwer, 1999.

[15] Vorob’ev, N N, A Constructive Propositional Calculus with Strong Negation (in Russian), Doklady Akademii Nauk SSR 85 (1952), 465– 468.

[16] Vorob’ev, N N, The Problem of Deducibility in Constructive Propositional Calculus with Strong Negation (in Russian), Doklady Akademii Nauk SSR 85 (1952), 689–692.