We summarize the foundations and applications of the new semantics called p-stable and we show that it holds the important property of extending the WFS semantics.
The research community has long recognized the study of non-monotonic reasoning (NMR) as a promising approach to model features of commonsense reasoning. On the other hand, monotonic logics have been successfully applied as a basic building block in the formalization of non-monotonic reasoning. In this direction, Veloso et al. [27] provide a precise treatment of notions such as 'generally', 'rarely', 'most', 'many', etc. in terms of logics of qualitative reasoning. These (monotonic) generalized logics, with simple sound and complete deductive calculi, are proper conservative extensions of classical first-order logic. Another line of research considers non-classical logics based on some form of logical completions. This paper explores some properties of one of the semantics based on this second formalization.
The stable semantics, which has been successfully used in the modeling of non-monotonic reasoning, was introduced by Gelfond and Lifschitz [11] by means of a simple transformation. More recently, a new semantics useful to model non-monotonic reasoning has been developed: the p-stable semantics. The original ideas that motivated this semantics can be found in [16]. Several works on the p-stable semantics have been done, some of the more relevant are [17,18,15,14,4,28,22].
In [18] the authors define the p-stable semantics for normal programs in terms of the G 3 logic and a construct called weak completion.
In [15] the authors generalize to disjunctive programs what was done in [18]. They introduce the p-stable semantics for disjunctive programs by means of a transformation similar to the one used by Gelfond and Lifschitz [11]. Thus, the p-stable semantics for normal and disjunctive programs can be expressed in two ways: in terms of a fixed point operator and classical logic after applying such transformation, and also in terms of the G 3 logic and weak completions. For this reason we refer to this semantics with either of the two names: p-stable or G 3 -stable semantics.
We emphasize that the p-stable semantics presented here, is a two-valued semantics that can be characterized by the three-valued logic G 3 . This semantics should not be confused with the partial stable semantics defined by Przymusinski [24].
This work has two main contributions, the first one corresponds to a summary about the foundations of the new semantics called p-stable which includes its applications and its relationship with paraconsistent logics. The second one corresponds to showing that the p-stable semantics holds the important property of extending the well founded semantics (WFS) defined in [26]. In this way we continue with the study of the p-stable semantics.
The structure of the paper is as follows: Section 2 tells about the foundations of the G 3 -stable semantics and some of its applications. Section 3 starts with basic background and definitions of the G 3 -logic, the p-stable semantics, the X-stable semantics for any logic X and programs with variables. In section 4, we review how the well founded semantics (WFS) can be induced by a powerful method called a Confluent LP-Systems CS [9]. Section 5 shows that the p-stable semantics extends the WFS semantics. Then, we present our conclusions.
This section is dedicated to review the p-stable semantics. We review its origins and foundations, its major known results, and some of its extensions. Although the contribution of this paper is not based on all the results presented in this section, we consider that it is worth to know more about the state of the art of this new semantics.
Recently, in [15] an approach for knowledge representation was proposed in terms of any paraconsistent logic stronger than or equal to C ω , the weakest paraconsistent logic introduced by da Costa [7]. The authors of [14] present a deep study of the paraconsistent logic G 3 which is a 3-valued logic. The matrices that define the logic G 3 were originally introduced by Carnielli et al. [6] only to prove that a certain formula is not a theorem in C w . In fact, the set of theorems of G 3 is a superset of the set of theorems of C w .
One interesting feature of the G 3 -logic presented in [14], is that it can be expressed in terms of the Lukasiewicz L 3 -logic, and vice-versa, the Lukasiewicz L 3 -logic can be expressed in terms of the G 3 -logic. In particular, G 3 can define the same class of functions as Lukasiewicz 3-valued logic and also can express very directly the strongest intermediate logic (also known as the Gödel's 3-valued logic) G 3 . In the same survey, the authors also prove that the logic G 3 admits a finite axiomatization, in fact, the one presented there consists of the axioms for C w plus four new axioms.
The authors of [18] introduce the p-stable semantics for normal programs, they also introduce the X-stable semantics for arbitrary programs and for any logic X. The construction used in this definition is called weak completion. The authors present several paraconsistent logics, all of them between C w , the weakest paraconsistent logic, and Pac, a well known maximal paraconsistent logic studied by Avron [1], and prove that the weak completions of all of these logics are equivalent to each other for normal programs. In [15] the authors establish this last result for disjunctive programs.
Weak completions have been used by D. Pearce [23] to characterize the stable semantics of disjunctive programs. Pearce's result states that weak completions of intermediate constructive logics (in particular G 3 logic and intuitionism) define the stable semantics of disjunctive programs.
In a parallel way, the p-stable semantics of disjunctive programs can be defined in terms of weak completions of paraconsistent logics, in particular G 3 [17,18]. It can also be expressed in terms of modal logics [17], and it can express the stable semantics of disjunctive programs [15].
We can say then, that two major classes of logics are successfully used to model NMR: constructive intermediate logics and paraconsistent logics. A well known semantics for modeling NMR is the stable semantics, which can be defined in terms of Intermediate logics. This semantics provides a fairly general framework for representing incomplete information and for reasoning with it. The p-stable semantics, which can be defined in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic.
[15] offers several results about the relation between the stable and the p-stable semantics, in particular every stable model of a normal program is also a pstable model, but the converse is not true as shown by the program a ← ¬a, which has {a} as its unique p-stable model and does not have stable models. The authors also give a sufficient condition on disjunctive programs for a stable model to be a p-stable model, we refer to this condition as "being closed under D-shifts", namely: a disjunctive program P is closed under D-shifts if for any of its disjunctive rules: H ← B + , ¬B − , and any a ∈ H, the rule a ← B + , ¬{B ∪ H − {a}} − also belongs to P . Then we have that any stable model of a disjunctive program closed under D-shifts is also a p-stable model of the program.
One of the main results presented in [15], is the fact that the G 3 -stable semantics is powerful enough to express the well known stable semantics of disjunctive programs; more precisely, the authors present a translation of a disjunctive program D into a normal program N, such that the p-stable model semantics of N corresponds to the stable semantics of D when restricted to the common language of the theories.
The G 3 -stable semantics shares properties with the stable semantics, but is closer to the semantics defined by classical logic. Consider the normal program P 1 : {a ← ¬b}.
The well known stable semantics by Gelfond et al. [11] of P 1 , as well as the G 3 -stable semantics give {a} as the unique intended model of this program. If we use classical logic we obtain {b} as a second model, but this is against the spirit of logic programming. Now, let us consider the following program P 2 : {a ← ¬b, a ← b, b ← a}. P 2 does not have stable models, but the set {a, b} is a model of P in classical logic. Indeed, this set is also the only G 3 -stable model of P 2 .
The main purpose of argumentation theory (Dung [10]), is to study the fundamental mechanism humans use in argumentation, and to explore ways to implement this mechanism on computers. Recently, in [4,19] it was shown that given an argumentation framework, its preferred semantics1 can be characterized by means of a normal program, such that the preferred extensions of the argumentation framework correspond exactly to the G 3 -stable models of the normal program. The three major semantics of argumentation theory (grounded, stable, and preferred) can be characterized in terms of three logic programming semantics: the well founded semantics (van Gelder et al. [26]), the stable semantics (Gelfond et al. [11]), and the p-stable semantics, respectively, in terms of a unique normal logic program P AF , which is constructed only in terms of the argumentation framework AF . P AF does not depend on any particular semantics. If we want to obtain the stable semantics of AF , we compute the stable semantics of logic programming over P AF . If, on the other hand, we want to obtain the preferred semantics of AF , we compute the p-stable semantics over P AF . Moreover, if we want to obtain the grounded semantics of AF , we compute the well founded semantics over P AF .
These results help to understand the close relationship between two successful approaches to non-monotonic reasoning: argumentation theory and logic programming with negation as failure.
In order to finish this brief motivation, we consider the expressivity of p-stable semantics. We mention three different approaches for knowledge representation based on this semantics: updates, preferences and argumentation (see previous section).
In case intelligent agents get new knowledge and this knowledge must be used to update the knowledge base, it is important to avoid inconsistencies. An update semantics for update sequences of programs based on G 3 -stable semantics is proposed in [20].
The concept of preferences is considered a vital component of reasoning with real-world knowledge. In [21], the authors introduce preference rules which allow to specify preferences as an ordering among the possible solutions to a problem. Their approach allows us to express preferences for arbitrary programs. They also define a semantics for those programs. The formalism used to develop their work is the G 3 -stable semantics.
Finally, we mention that the theory of the p-stable semantics is closely related to topics that have been active areas of research: The theory of paraconsistent logics, the theory of ground non-monotonic modal logics, and the theory of weak completions created by D. Pearce to characterize the stable semantics of disjunctive programs in terms of constructive intermediate logics.
Thus, the G 3 -stable semantics is one of several semantics defined by a family of paraconsistent logics, all of which define the p-stable semantics when restricted to disjunctive programs.
Since the present work continues the study of the p-stable semantics, we review the background necessary to understand the definition of the p-stable semantics. In this way, this section summarizes the G 3 logic, however some different results of the p-stable semantics are related to other logics; we present here some basic background about these logics. We also present some important definitions useful to understand this work.
A signature L is a finite set of elements that we call atoms, or propositional symbols. The language of a propositional logic has an alphabet consisting of proposition symbols: p 0 , p 1 , . . . connectives: ∧, ∨, ←, ¬ auxiliary symbols: (, ), where ∧, ∨, ← are 2-place connectives and ¬ is a 1-place connective. Formulas are built up as usual in logic. If F is a formula we will refer to its signature L F as the set of atoms that occur in F . The formula F ≡ G is an abbreviation for (F ← G) ∧ (G ← F ). The formula A ← B is just another way of writing B → A. A literal is either an atom a, or the negation of an atom ¬a.
When a formula is constructed as a conjunction (or disjunction) of a set of literals , F = (or F = ), we denote by Lit(F ) such set of literals. A clause is a formula of the form H ← B (also written as B → H), where H and B, arbitrary formulas in principle, are known as the head and body of the clause respectively. The body of a clause could be empty, in which case the clause is known as a fact and can be noted just by: H ←. In the case when the head of a clause is empty, the clause is called a constraint and is noted by: ← B.
A normal clause is a clause of the form a ← (B + ∪ ¬B − ) where a is an atom, and B + , B − are, possibly empty, sets of atoms. A disjunctive clause is a clause of the form H ← (B + ∪ ¬B − ) where H is a set of atoms, and B + , B − are, possibly empty, sets of atoms.
The symbol ¬, before one of such sets, denotes the conjunction of the negations of the atoms belonging to the set. Sometimes a disjunctive clause may be written as H ← B + , ¬B − following typical conventions for logic programs, similarly for normal clauses. A definite program is a normal program whose rules do not have negations in their bodies.
Finally, a program is a finite set of clauses. If all the clauses in a program are of a certain type, we say that the program is also of that type. For instance a set of disjunctive clauses is a disjunctive program, a set of normal clauses is a normal program and so on.
For arbitrary programs, and proper subclasses, we will use HEAD(P ) to denote the set of all atoms occurring in the heads of the clauses of P .
Let P rog L be the set of all normal programs with atoms from the signature L. A partial interpretation based on a signature L is a disjoint pair of sets
Given two interpretations
Clearly ≤ k is a partial order. We may also see an interpretation I 1 , I 2 as a set of literals I 1 ∪¬I 2 . When we look at interpretations as sets of literals then ≤ k corresponds to ⊆.
A general semantics SEM is a function on P rog L which associates with every program a partial interpretation. Given a signature L and two semantics SEM 1 and SEM 2 , we define
Next, we proceed to give definitions of the relevant logics and semantics.
The G 3 logic is a 3-valued logic with truth values in the domain D = {0, 1, 2} where 2 is the designated value. The evaluation functions of the logic connectives are then defined as follows: x ∧ y = min(x, y); x ∨ y = max(x, y); the ¬ and → connectives are defined according to the truth tables given in Table 1.
We define a tautology as any formula that takes only the designated value 2, regardless of what the truth values the atoms in the formula may take. We will use the notation |= G 3 A, to express the fact that A is a tautology in G 3 . We must notice the subtle difference between the logic G 3 and the best known logic G 3 due to Gödel; the latter is defined exactly by the same functions as the former, except that the negation corresponding to the truth value 1 is 0.
As a consequence, whereas G 3 accepts the principle of the excluded middle, G 3 does not. An axiomatization for G 3 is presented in [14]. In particular all of the axioms of C w are included in such axiomatization. Modus Ponens is the only rule of inference. We will use the notation G 3 A, to express the fact that the formula A is a theorem in G 3 ; i.e. A can be inferred from the axioms of G 3 , by using modus ponens.
Positive Logic is defined by the following set of axioms:
G 3 is defined by all axioms of positive logic plus the following six axioms:
In order to simplify notation, we use A ∨ B as an abbreviation for ((A → B) → B) ∧ ((B → A) → A) in the first of the new six axioms, and in the last axiom we use the abbreviation: ∼ A := A → (¬A ∧ ¬¬A).
One of the main results presented in [14], is a soundness and completeness theorem for the G 3 logic, namely: a formula is a tautology in the three-valued logic G 3 if and only if, it is a theorem according to the axiomatization; we can express this in the notation we have introduced: |= G 3 A if and only if G 3 A. We will use any of the two terminologies when referring to such a formula. Positive logic plus the two axioms: A ∨ ¬A and ¬¬A → A, define the C w logic, the weakest paraconsistent logic defined by da Costa [7].
We observe that the formula (¬A ∧ A) → B is not a theorem in either of the two logics. This fact indeed makes these two logics paraconsistent. The G 3 logic is strictly stronger than C w , and both of them are strictly weaker than classical logic. In particular the formula B → [(¬B ∧ A) → C], where A,B and C are arbitrary formulas, which is a tautology in classical logic, is not always a tautology in G 3 , as is seen in the particular case when A, B, C take the truth values of 2,1 and 0 respectively. As a useful result we also mention that the formula (¬A → A) → A is a tautology in the G 3 logic for any formula A.
These two axioms allow to do proofs by contradiction but in some limited way; other constructions such as the law of the excluded middle: (A ∨ ¬A), are not valid in intuitionistic logic; however the formula (¬A ∧ A) → B is valid in this logic. All of these properties are shared with the logic G 3 mentioned before; in fact, G 3 is stronger than I in the sense that any theorem in I is also a theorem in G 3 .
Notice the opposite situation occurring between intuitionistic and G 3 logics, and the paraconsistent logics C w and G 3 regarding the last two formulas above; as it was mentioned before, the first one is valid in C w and G 3 , but the second one is not. See van Dalen [25] for a good introduction to intuitionistic logic. We will use the following notation: |= denotes the consequence relation in classical logic, X denotes the inference relation in any particular logic X. For any two formulas A and B, A ≡ X B denotes the fact that A and B are equivalent in logic X, i.e. A → B and B → A are both theorems or tautologies in logic X, depending on how logic X is defined. Two programs P and Q are equivalent in logic X, denoted: P ≡ X Q, if the conjunction of the rules in P is equivalent, in logic X to the conjunction of the rules in Q. As a known fact, we observe that the first two axioms of positive logic guarantee the deduction theorem, namely: for Γ, A, B, where Γ is a set of formulas, and A, B are formulas: Γ, A B if and only if Γ A → B.
From now on we assume that the reader is familiar with the notion of classical minimal model, Lloyd [13].
Here we define the p-stable semantics for disjunctive programs.
Definition 1. [15] Let P be a disjunctive program and M be a set of atoms. We define: For convenience and to be consistent with the definition of a semantics SEM as a function on P rog L which associates with every program a partial interpretation, from now on, we denote a p-stable model M of a disjunctive program P as a pair M, L P \ M . We know, that this is not a standard way to represent the p-stable semantics, however this will be useful to present the contribution of this paper.
The following examples illustrate how to obtain the p-stable models of different programs. Our first example shows a disjunctive program with two p-stable models. The next example shows a program with a single p-stable model, which is also a classical model.
Example 2. Let P be the normal program: q ← ¬q. Let us take M = {q} then RED(P, M ) is the following program: q ← ¬q. It is clear that M models P in classical logic and RED(P, M ) |= M since (¬q → q) → q is a theorem in classical logic with the negation ¬, now interpreted as classical negation. Therefore M is a p-stable model for P .
Our third example shows a program which has several classical models but has no p-stable models.
c} are all models of P in classical logic. However, they are not p-stable models of P . If we apply definition 2 to M 4 , we have RED(P, M 4 ) = P and M 4 models P in classical logic, however RED(P, M 4 ) |= M 4 . If we apply definition 2 to M 1 , we obtain RED(P, M 1 ) as the following program: {a ← ¬b, b ←, c ← ¬a} and it is clear that M 1 models in classical logic each of the rules of P . However, the second condition in definition 2 is not satisfied, since RED(P, M 1 ) |= a. By symmetry the same result is obtained for M 2 and M 3 . Hence, the program does not have p-stable models.
Finally, we present a program which has no stable models and whose p-stable and classical models are the same.
Example 4. Let P be the normal program: {a ← ¬b, a ← b, b ← a}. We can verify that M = {a, b} models the rules of P in classical logic. From the definition of the RED transformation, we find that RED(P, M ) = P . Now, from the first and third rule, it follows that (¬b → b) where the negation ¬ is now interpreted as classical negation. Since (¬b → b) → b is a theorem in classical logic, it follows that P |= M . Therefore, M is a p-stable model of P .
Now we review a characterization of the p-stable semantics for disjunctive programs in terms of the G 3 logic. First we present some useful definitions.
Given a program P and a set of atoms M ⊆ L P , we call the construct P ∪ ¬M c a weak completion of the program P (with respect to the set of atoms M ), where the superscript c, denotes set theoretical complement operator with respect to L P . Definition 3. Let P be any theory, X be any logic and M be a set of atoms. M is a X-stable model of P if the next two conditions hold: X P ∪ ¬M c → M and M is a classical model of P .
The expression appearing in the first condition of this definition is interpreted as the formula where the antecedent is the conjunction of all rules in P and all literals in ¬M c , and the consequent is the conjunction of all the atoms in M . We will keep using this interpretation in what follows.
Of particular interest to us is the G 3 -stable semantics, which is the result of using the logic G 3 in the previous definition. For more details see [5].
Example 5. Consider the following logic program: P = {b ← ¬a, a ← ¬b, p ← ¬a, p ← ¬p}. It is easy to verify that this program has two G 3 -stable models, which are {a, p} and {b, p}.
Theorem 1 gives a characterization of the p-stable semantics for disjunctive programs in terms of the G 3 logic. This result was first proven for normal programs in [18]; more recently it has been extended to disjunctive programs in [15]. Theorem 1. [15] Let P be a disjunctive program and M be a set of atoms. M is a p-stable model of P iff M is a G 3 -stable model of P .
As can be seen, p-stable models are defined for propositional logic programs only. However this definition can be extended to predicate programs, which allows the use of predicate symbols in the language, but without function symbols to ensure the ground instance of the program to be finite. So a term can only be either a variable or a constant symbol. The ground instance of a predicate program P , Ground (P ), is defined in Lifschitz [12] as the program containing all ground instances of clauses in P . Then M is defined as a p-stable model of a predicate program P if it is a p-stable model for Ground (P ).
The following section review the WFS semantics in order to show that the pstable semantics holds the important property of extending the WFS semantics. Since the definition of WFS for normal programs is unique and has been accepted by the research community, as opposed to the case of disjunctive programs, from now on we deal exclusively with normal propositional logic programs.
In this section we review how the well founded semantics (WFS) can be induced by a powerful method called a Confluent LP-System CS [9]. This method does not only characterize well-known semantics for logic programs but can be used to define new semantics. Roughly speaking, a semantics for a class of logic programs determines the set of derivable literals for each program P . The method of determining such a semantics is to rewrite the program P according to certain rewriting rules until we arrive at a normalform of the original program from which we can immediately read off the derivable literals. Suitable sets for rewriting rules correspond to different normalforms and thus to different semantics.
The theory of Confluent LP-Systems CS [9] combines methods from rewriting systems with logic programming technology to define a powerful framework for investigating the semantics of logic programs. The starting point of this theory is to determine a set of rewriting rules that is confluent and that computes the semantics in a canonical way. These rules transform programs into simpler programs. Confluence and termination guarantee that every program has associated with it a normalform. This normalform then induces a semantics and a simple and efficient method to answer queries with respect to this semantics.
It is important to note that Confluent LP-Systems CS correspond to a general theory, i.e., the concept is not attached to any particular semantics. [9] shows how most of the classical semantics such as Fitting's 3-valued version of Clark's completion, the wellfounded semantics WFS and Schlipf's extension WFS + can be defined as a Confluent LP-System in a natural way.
The following definition plays an important role to define the semantics of a normal program based on the notion of a rewriting system [9]. Definition 4. [9] For any normal program P we define SEM min (P ) = P true , P f alse where P true := {p | p ← ∈ P }, P f alse := {p | p ∈ L P \ HEAD(P )}. Now we define a rewriting system, normalform, and some properties of rewriting systems. Definition 5. [9] An abstract rewriting system is a pair S, → where → is a binary relation on a given set S. Let → * be the reflexive, and transitive closure of →. When x → * y we say that x reduces to y. An irreducible element is said to be in normalform. We say that a rewriting system is noetherian: If there is no infinite chain x 1 → x 2 → . . . → x i → x i+1 → . . ., where for all i the elements x i and x i+1 are different, confluent: If whenever u → * x and u → * y then there is a z such that x → * z and y → * z.
In a noetherian and confluent rewritten system, every element x reduces to a unique normalform that we denote by norm(x) [9].
The main concept on which the notion of a Confluent LP-Systems CS is based, is the concept of a transformation rule.
A transformation rule is a binary relation on P rog L . Let a program P ∈ P rog L be given. We define the following transformation rules. RED + : This transformation can be applied to P , if there is an atom a which does not occurs in HEAD(P ). RED + transforms P into the program where all Definition 8. [3] Let CS 1 be the Confluent LP-System which contains the following transformation rules: RED + , RED − , Success, Failure, and Loop.
The Confluent LP-System CS 1 induces the WFS semantics. Theorem 2. [9] The WFS semantics is the semantics induced by the Confluent LP-System CS 1 .
The W F S + semantics is an extension of WFS introduced in [8]. We present a Confluent LP-System CS 2 used to compute the W F S + semantics given in [3].
Here, we show that the p-stable semantics extends the WFS + and specially the WFS semantics. These results are based on the fact that the p-stable semantics for disjunctive and in particular for normal programs is invariant under each of the transformations that define the Confluent LP-Systems CS 1 and CS 2 [5].
The following theorem indicates that the p-stable semantics is consistent with the WFS + semantics. Proof. Let P → P 1 → . . . → P n be the chain of reductions in the Confluent LP-System CS 2 that leads to the normalform P n = norm CS 2 (P ). Then we have SEM min (P ) ≤ k SEM min (P 1 ) ≤ k . . . ≤ k SEM min (P n ) = W F S + (P ).
Since the p-stable semantics is invariant under any of the transformations that define the Confluent LP-System CS 2 , then M, L P \ M is a p-stable model of each of the programs P, P 1 , . . . , P n .
For any fact a ← ∈ P , it follows that a ∈ M according to remark 1, hence T ⊆ M . By the same remark 1, M ⊂ HEAD(P n ), therefore L P \ HEAD(P n ) ⊂ L P \ M . Thus we have T, F ≤ k M, L P \ M .
Since the p-stable semantics is an extension of WFS + and WFS + is an extension of WFS, a corollary of theorem 4 indicates that the p-stable semantics is also an extension of WFS semantics. Proof. All transformations that define the WFS semantics are contained in those that define the WFS + semantics. Let P → P 1 → . . . → P s be a chain of reductions that leads to the normalform P s = norm CS 1 (P ). This chain can be extended to P → P 1 → . . . → P s . . . → P n so that P n = norm CS 2 (P ), where n ≥ s. Then we have SEM min (P s ) ≤ k SEM min (P n ), i.e., SEM CS1 (P ) ≤ SEM CS2 (P ). Then the result follows from Theorem 4.
We showed that the p-stable semantics extends the well known WFS semantics. This result is based on the fact that WFS can be induced in a natural way by a confluent LP-system, which is based on certain transformations rules; and on the fact that the p-stable semantics for normal programs is invariant under each of these transformations.
occurrences of ¬a are removed. RED − : This transformation can be applied to P , if there is a rule a ← ∈ P . RED − transforms P into the program where all clauses that contain ¬a in their bodies are deleted. SUB (Subsumption): This transformation can be applied to P , if P contains two clauses a ← body 1 , a ← body 2 where body 1 ⊆ body 2 . SUB transforms P into the program where the clause a ← body 2 has been removed. Success: Suppose that P includes a fact a ← and a clause q ← body such that a ∈ body. Then we replace the clause q ← body by q ← body \ {a}. Failure: Suppose that P contains a clause q ← body such that a ∈ body and a ∈ HEAD(P ). Then we erase the given clause. LC (Logical consequence): Suppose P |= a for an atom a. Then we can add the rule a ← to P . Loop: We say that P 2 results from P 1 by Loop w.r.t. A if, by definition, there is a set A of atoms such that
Although these transformation rules are not really functions on P rog L (e.g. RED − is only determined if an occurrence of a certain rule is distinguished), they induce a set of operators on P rog L [9]. An operator, denoted as op, is a function over the set of programs that transforms a program P into a program P op as follows. If C 1 , C 2 are clauses, g is a literal and f is an atom, then op can be of type Red + , then P op is the reduction of P with respect to C 1 and g. We write RED + , C 1 , g [9].
We could define in a similar way the operators for the other transformations.
Example 6. [9] If P is {c ← ¬d} and op1 is RED + , ¬d ←, c ← ¬d then P op1 is {c ←}. If op2 is RED + , c ← ¬d, ¬c then P op2 = P .
Next, we give the definition of Confluent LP-System CS.
A Confluent LP-System CS over the signature L is a pair {op i | i = 1, . . . , n}, → that satisfies the following conditions: 1. {op i | i = 1, . . . , n} is a finite set of transformation rules on P rog L . By abuse of language we often view them as (computable) operators as we explained before. 2. P rog L , → , where → is the union of all the transformation rules in CS, is a noetherian and confluent rewriting system. 3. If P → P 1 then SEM min (P ) ≤ k SEM min (P 1 ).
We denote the uniquely determined normalform of a program P with respect to the Confluent LP-System CS by norm CS (P ) [9].
Every Confluent LP-System CS induces a semantics SEM CS as follows [9]: SEM CS (P ) := SEM min (norm CS (P )). Now, we present a Confluent LP-System CS 1 used to compute the WFS semantics in quadratic time and introduced in [3].