Given a propositional formula X, we present a mapping that constructs a general program P, such that the maximal models of X correspond to the stable models of P, after intersecting each stable model with the relevant atoms. Maximal models are of interest for di erent applications.
Generating maximal models of a propositional formula is of interest in di erent
applications. For instance, it has been shown that in argumentation theory the
preferred semantics of an argumentation framework can be expressed in terms
of maximal models of a propositional formula [
Given a propositional formula X, we present a mapping that constructs a
general program P, such that the maximal models of X correspond to the stable
models of P, after intersecting each stable model with the relevant atoms. We
present this mapping as a sequence of basic steps in a way that they represent a
simple methodology that can be applied to any problem of this nature. In fact,
we can infer the maximal models of a formula by using disjunctive answer set
solvers e.g., DLV [
The rest of the paper is divided as follows: In 2, some basic concepts of logic programs and stable model semantics are presented. In 3, our characterization of the maximal models in terms of stable models is presented. Finally in the last section, we present our conclusions. 2.1
The language of a propositional logic has an alphabet consisting of (i) proposition symbols: p0; p1; ::: (ii) connectives : _; ^; Ã; :; ?; > (iii) auxiliary symbols : ( , ). where _; ^; Ã are binary connectives, : is an unary connective and ?; > are zeroary connectives. The proposition symbols and ? stand for the indecomposable propositions, which we call atoms, or atomic propositions. A literal is an atom, a, or the negation of an atom :a. Given a set of atoms fa1; :::; ang, we write :fa1; :::; ang to denote the set of literals f:a1; :::; :ang: Formulas are constructed as usual in logic. A theory T is a nite set of formulas. By LT , we denote the signature of T , namely the set of atoms that occurs in T.
A general clause, C, is denoted by a1 _ : : : _ am à l1; : : : ; ln,3 where m ¸ 0, n ¸ 0, each ai is an atom, and each li is a literal. When every literal li is an atom, the clause is considered positive. When n = 0 and m > 0, the clause is an abbreviation of a1 _ : : : _ am à >, where > is :?. When m = 0 the clause is an abbreviation of ? à l1; : : : ; ln. Clauses of this form are called constraints (the rest, non-constraint clauses). A general program, P , is a nite set of general clauses. A positive general program P is a nite set of positive general clauses. A given program f®1; :::; ®ng is also represented as f®1; :::; ®ng to avoid ambiguities with the use of the comma in the body of the clauses.
We point out that whenever we consider logic programs our negation : corresponds to the default negation not used in Logic Programming. Also, it is convenient to remark that in this paper we are not using at all the so called strong negation used in ASP. 2.2
First, to de ne the stable model semantics, let us de ne some relevant concepts. De nition 1. Let T be a theory. An interpretation I is a mapping from LT to f0; 1g meeting the conditions: 1. I(a ^ b) = minfI(a); I(b)g, 2. I(a _ b) = maxfI(a); I(b)g, 3. I(a à b) = 0 if and only if I(b) = 1 and I(a) = 0, 4. I(:a) = 1 ¡ I(a), 5. I(?) = 0. 6. I(>) = 1.
It is standard to provide interpretations only in terms of a mapping from LT to f0; 1g. But then it is easy to prove that it is unique by virtue of the de nition by recursion. 3 l1; : : : ; ln represents the formula l1 ^ ¢ ¢ ¢ ^ ln.
An interpretation I is called a model of P if and only if for each clause c 2 P , I(c) = 1. Given a theory T and a formula ®, we say that ® is a logical consequence of T , denoted by T j= ®, if for every model I of T we have I(®) = 1. A theory (or a formula) is consistent if it admits a model, otherwise it is said to be inconsistent. It is well known that T j= ® i T [ f:®g is inconsistent.
It is possible to identify an interpretation with a subset of a given signature. For any interpretation, the corresponding subset of the signature is the set of all atoms that are true with respect to the interpretation. Conversely, given an arbitrary subset of the signature, there is a corresponding interpretation de ned by specifying that the mapping assigned to an atom in the subset is equal to 1 and otherwise to 0. We use this view of interpretations freely in the rest of the paper.
We say that a model I of a theory T is a minimal model if it does not exist a model I0 of T di erent of I such that I0 ½ I. Maximal models are de ned in the analogous way.
By using answer set programming, it is possible to describe a computational
problem as a logic program whose answer sets correspond to the solutions of the
given problem. The stable model semantics was rst de ned in terms of the so
called Gelfond-Lifschitz reduction [
Let P be any general program. For any set S µ LP , let P S be the general program obtained from P by deleting (i) each rule that has a formula :l in its body with l 2 S, and then (ii) all formul of the form :l in the bodies of the remaining rules. Clearly P S is positive, then S is a stable model of P if and only if S is a minimal model of P S . However, note that P S may contain constraints. 3
In this section, we provide a method for obtaining maximal models of a propositional theory in terms of stable models of a general program.
De nition 2. Let L be a signature. Let L0 be a new signature (namely L \ L0 = ;) of the same cardinality as L that of course admits a bijective function f from L to L0. We say in this case that L0 is a copy-signature of L. In addition, we write f (a) (or also a²) to denote the image of a under f . For a given set of atoms N , we write f (N ) to denote the set ff (a) : a 2 N g.
Note that if L0 is a copy-signature of L then also L is a copy-signature of L0.
To explain the methodology of this section, we use a simple formula as a running example. Let our theory be T1 := fa _ b; :bg. Note that fag is the unique maximal model of our theory.
One can establish an important relationship between maximal and minimal models. The proof is straightforward.
Lemma 1. Let T be a theory with signature L and L0 be a copy-signature of L. By g(T ) we denote the theory obtained from T by replacing every occurrence of an atom x in T by :f (x). Then M is a maximal model of T i f (L n M) is a minimal model of g(T ).
Let us come back to our example. Note that g(T1) := f:a² _ :b²; ::b²g. The complement of fag (maximal model of T1) w.r.t. to fa; bg is fbg. Now, f (fbg) is fb²g, that is precisely the minimal model of g(T1).
The second step is conceptually very simple. Transform the new theory R := g(T ) into a logically equivalent positive general program, denoted by general(R) or just P . This is of course always possible using well known basic logical transformations. In our case g(T1) is transformed to P1 := f? Ã a²; b²; b²g. Clearly, g(T ) and P have the same set of minimal models. Moreover, the set of stable models of P are the same as the set of minimal models of g(T ).
For the third and nal step we need to state the following lemma. Lemma 2. Let S be a general program of the form S1 [S2, where S1 is a positive general program with signature L and S2 := fx² Ã :x : x 2 Lg such that L0 is a copy-signature of L. Then M is a stable model of S i there exists a minimal model N of S1 such that M = N [ f (L n N ).
Let us come back again to our example. Recall that P1 := f? à a²; b²; b²g. The signature of P1 is fa²; b²g and the copy-signature is fa; bg Now consider the general program P2 := P1 [ fa à :a²; b à :b²g. The unique stable model of P2 is fb²; ag. We could obtain this model as follows: obtain a minimal model of P1, getting fb²g. Now, the complement of this model is fa²g, and f (fa²g) is fag. Finally we obtain fb²g [ fag as desired. Hence if this model is intersected with the original signature, we obtain our desired maximal model of the original theory.
Let us summarize our approach. We are given T1 := fa _ b; :bg. We want to obtain a maximal model of T1. We rst construct the program g(T1) := f:a² _ :b²; ::b²g. Then we compute the associate positive general program P1 := f? à a²; b²; b²g. Now we add P2 := P1 [ fa à :a²; b à :b²g. Compute a stable model of P2 using DLV. We obtain fb²; ag. Intersect it with the original signature and we get fag. This is a maximal model of T1, as desired.
We are grateful to anonymous referees for their useful comments. Juan Carlos Nieves wants to thank CONACyT for his PhD Grant. 4
We have presented a methodology to transform a problem of generating maximal models into the problem of obtaining stable models of a general program. As a consequence we can generate the maximal models of a formula by using disjunctive answer set solvers e.g., DLV.