In recent work, we provided a formulation of ASP programs in terms of linear logic theories. Answer sets were characterized in terms of maximal tensor conjunctions provable from such theories. In this paper, we propose a full comparison between Answer Set Semantics and its variation obtained by interpreting literals (including negative literals) as resources, which leads to a different interpretation of negation. We argue that this novel view can be of both theoretical and practical interest, and we propose a modified Answer Set Semantics that we call Resource-based Answer Set Semantics. One advantage is that of avoiding inconsistencies, so every program has a (possibly empty) resource-based answer set. This implies however the introduction of a different way of representing constraints.
In [
We proved in particular that RASP (and thus, ASP as a particular case) corresponds
to a fragment of linear logic. This was done by providing a two-ways translation of
RASP programs into a linear logic theory. The result implies that a RASP inference
engine (such as Raspberry [
In the present paper, we show that understanding default negation as a resource
goes beyond, and leads to the definition of a generalization of the answers set semantics
(for short AS, on which ASP is based), with some potential advantages. We provide a
? A short version of this paper will appear in the Proc. of LPNMR 2013. This research is partially
supported by GNCS-13 project.
model-theoretic definition of the new semantics, that we call Resource-based Answer
Set Semantics. In the new setting, there are no inconsistent programs, and basic odd
cycles (similarly to basic even cycles in AS) are interpreted as exclusive disjunctions.
Constraints must then be represented explicitly (while in ASP they are “simulated” via
unary odd cycles). Therefore, what was before programs with constraints becomes a
plain ASP program (under the extended semantics) augmented with a set of explicitly
represented constraints. We argue that representing constraints separately can lead to
more generality and to an improved elaboration-tolerance (in the sense of [
The paper is organized as follows. In Sections 2 and 3, we provide the necessary
background on linear logic and ASP. In Section 4, we specialize the method defined in
[
Linear logic [
In linear logic, contraction and weakening rules are not allowed: hence, while a
statement of the form P → P ∧ P is valid in classical logic, this is not the case in
linear logic. The point here can be explained by observing that in classical logic
statements are assumed to express “static” properties, unchanging facts about the world.
On the contrary, linear propositions are concerned with dynamic properties of finite
amounts of resources (and the processes that use them). An example well-known in
the literature [
P : “ One dollar” Q : “ One pack of Camel” R : “ One pack of Marlboro”
P → Q
P → R
assuming the mentioned interpretation of propositions as resources (and of implications as transformation processes, very much like in RASP).
One of the crucial features of linear logic is that it makes a neat distinction between two forms of conjunction that are not distinguished by classical logic. Namely, one of them intuitively means “I have both”. This is said multiplicative conjunction and is written as ⊗. The other, the additive conjunction means “I have a choice” (and is written as &). Dually, there are two disjunctions. The multiplicative one, written P O Q can be read as “if not P, then Q”, and the additive disjunction P ⊕ Q, that intuitively stands for the possibility of either P or Q, but we do not know which of the two. That is, it involves “someone else’s choice”.
cess: it can be read as “ Q can be derived using P exactly once”. (Notice that, in such a process P is “consumed”, so it cannot be used again.)
Linear negation ⊥ is the only negative operation in the logic. It is involutive (namely, (P⊥)⊥ and P can be safely identified) and, at the same time, it retains a constructive character. Notice that it acts as a sort of transposition: P — ◦ Q coincides with
In order to re-gain the full power of classical logic exponential operators, namely ! and its dual ?, are introduced. Intuitively, !P means that we have how many P we want. These connectives reintroduce, in a more controllable way, contraction and weakening in the logical framework.
To better illustrate all these connectives, let us recall another example (taken
from [
For a fixed-Price Menu: 5 Dollars (D) you can have:
Hamburger (H)
Coke (C)
All the french fries (F) you can eat
One between Onion-Soup (O) or Salad (S)
Pie (P) or Ice-Cream (I) depending on availability and its encoding in a linear logic formula: (D ⊗ D ⊗ D ⊗ D ⊗ D) — ◦
H ⊗C ⊗ !F ⊗ (O & S) ⊗ (P ⊕ I)
Some further notions will be used in what follows. Let X s and Y s denote tensor products of positive literals, e.g. formulas of the form (P1⊗ · · · ⊗Pn) (for n > 0). Then, generalized Horn implications are defined as follows: – an Horn implication has the form: X — ◦Y . – An ⊕-Horn implication has the form: X1 — ◦ (Y1 ⊕ Y2) .
– An &-Horn implication has the form: (X1 — ◦Y1) & (X2 — ◦Y2) .
terministical process where a choice is made between the two disjuncts (say P2 — ◦ Q2) and then the (sub-)process encoded by the selected option is executed (in our case Q2 is produced using P2).
A formal proof system for linear logic can be formulated in terms of a Gentzen-style
sequent calculus. A sequent is composed of two sequences of formulas separated by a
turnstile (`) symbol. The sequent Δ ` Γ asserts that the multiplicative conjunction of
the formulas in Δ together imply the multiplicative disjunction of the formulas in Γ .
In general, a sequent calculus proof rule consists of a set of hypothesis sequents and a
single conclusion sequent. A full set of Gentzen-style sequent rules for linear logic can
be found, for instance, in [
In the answer set semantics (originally named “stable model semantics”), a (logic)
program Π (cf., [
Various extensions to the basic paradigm exist, that we do not consider here as they
are not essential in the present context. We do not even consider “classical negation”
(cf., [
In the rest of the paper, whenever it is clear from the context, by “a (logic) program Π ” we mean an answer set program (ASP program) Π , and we will implicitly refer to the “ground” version of Π . The ground version of Π is obtained by replacing in all possible ways the variables occurring in Π with the constants occurring in Π itself, and is thus composed of ground atoms, i.e., atoms which contain no variables. By “minimal model of Π ” we mean a minimal model of Π intended as a classical logic theory, where ← is intended as implication and not as negation in classical logic terms.
The answer sets semantics [
Unlike other semantics, a program may have several answer sets, or may have no
answer set. Whenever a program has no answer sets, we will say that the program is
inconsistent. Correspondingly, checking for consistency means checking for the existence
of answer sets. The following program has no answer set: {a ← not b. b ← not c. c ←
not a.}. The reason is that in every minimal model of this program there is a true atom
that depends (in the program) on the negation of another true atom, which is strictly
forbidden in this semantics, where every answer set can be considered as a self-consistent
and self-supporting set of consequences of given program. The program {p ← not p.}
has no answer sets either as it is contradictory. Constraints of the form defined above can
be simulated by plain rules of the form p ← not p, L1, . . . , Ln. where p is a fresh atom.
Thus, consistency is related (as discussed at length in [
Below is the specification of the Answer Set Semantics, reported from [
Answer sets are defined as follows.
Definition 2. Let I be a set of atoms and Π a program. I is an answer set of Π iff ΓΠ (I) = I.
It will be useful in what follows to report from [
Answer sets are in fact minimal supported models, and non-empty answer sets form an anti-chain with respect to set inclusion.
In the ASP (Answer Set Programming) paradigm, each answer set is seen as a
solution of given problem, encoded as an ASP program. To find these solutions, an
ASPsolver is used. Several solvers have became available, see [
In this section, we specialize the method defined in [
2 The property holds for models in general, but minimal ones are those of interest here.
A positive ASP program Π (i.e., a program without default negation) can be transformed into a corresponding Linear Logic RASP Theory as follows (notice that the reverse translation is also possible, i.e., to transform a Linear Logic RASP Theory into a (R)ASP program). In particular, in the definition below each atomq in the body of the j-th rule of given program is renamed as q j, where the q j’s are called the standardizedapart versions of q. Moreover, since the formalization passes through RASP, which considers atoms as resources, each standardized-apart atom q j will stand for q j:1 (In RASP terminology, a writing of the form q:a denotes an amount a of the resource q.). The meaning is that, when using the body of a rule to derive the head, one uses one unit of each atom (seen as a resource) in the body3. Notice that, in Π , the truth of an atom might be used to prove several consequences (through different rules). As we mentioned before, linear logic provides the exponential connective !A, intuitively meaning that we can use as many occurrences of A as we want. However, exploiting this connective would bring us outside the finite propositional fragment of linear logic at hand. The devised method remains within the propositional fragment.
Definition 3. Given a positive ASP program Π , the corresponding Linear Logic RASP Theory ΣΠ is obtained by applying, in sequence, the following rewritings. – Standardize apart the atoms in the bodies of rules of Π . Namely, each occurrence of an atom A in the body of the j-th rule is replaced by A j:1. – For every atom A occurring as head of h > 0 rules in (the standardize apart version of) Π , let A ← Bi,1, . . . , Bi,`i , for i = 1, . . . , h, be such rules (with `i possibly null, if the corresponding rule is a fact). Replace these rules by the following linear implications (where the Ais are fresh atoms):
Bi,1⊗ . . . ⊗ Bi,`i — ◦ Ai A1 & . . . & Ah — ◦ A for i = 1, . . . , h – For each atom A, let A1:1, . . ., Am:1 be its standardized apart versions, introduced as described earlier. Add to ΣΠ the linear implication A — ◦ A1:1 ⊗ . . . ⊗ Am:1. – Replace in ΣΠ any linear implication B1 ⊗ . . . ⊗ Bn — ◦ H with the implication
B1 ⊗ . . . ⊗ Bn — ◦ H ⊗ B1R ⊗ . . . ⊗ BnR.
Let us remark some aspects of the previous definition. Notice that through the second step of the translation, the body of each rule in Π , which is a conjunction of atoms, is turned into a tensor conjunction of atoms. The purpose of the linear implication
of the) rules defining it. Clearly, the introduction of such an implication can be avoided in case A occurs as head of a single rule (in this case h = 1 and we can simply replace A1 by A in the first linear implication). In what follows we will adhere to this convention whenever possible.
tions with a unique conjunct. It models the fact that A is a resource available to any rule that may need to use it.
3 RASP allows for arbitrary quantities, not needed here.
Notice, moreover, the introduction of a fresh atom BiRs corresponding to each atom Bi, in the last step of the translation. These fresh atoms are called the r-copies of the Bis. They are produced just in order to keep a record of those resources that have been consumed. R-copies allow us to establish a correspondence between answer sets of Π and maximal tensor conjunctions provable from ΣΠ , where: Definition 4. Given linear logic theory Σ , a tensor conjunction of atoms A1 ⊗ . . . ⊗ An (n ≥ 0), is called maximally provable if it is provable from Σ , and for any atom B, the tensor conjunction A1 ⊗ . . . ⊗ An ⊗ B is not provable from Σ (we equivalently talk about a maximal tensor conjunction provable from Σ ).
Lemma 1. Let Π be a positive ASP program Π , and ΣΠ be the corresponding Linear Logic RASP Theory. Every maximal tensor conjunction A provable from ΣΠ includes all the r-copies of facts of ΣΠ and of standardized-apart atoms occurring in the body of linear implications of ΣΠ that have been used for proving atoms in A .
As mentioned, the role of r-copies is to keep records of facts (intended as resources originally present in the program) and of intermediate conclusions used (as resources) in further inference. In a linear-logic setting in fact, resources which are consumed “disappear”, thus we would not be able to establish a relation between provable tensor conjunctions and answer sets. Now in fact, we are able to state (neglecting, by abuse of notation, the syntactic distinction between an atom A and its r-copy AR): Theorem 1. Let Π be a positive ASP program Π , and ΣΠ be the corresponding Linear Logic RASP Theory. A1 ⊗ . . . ⊗ An is a maximal tensor conjunction provable from ΣΠ if and only if {A1, . . . , An} is an answer set for Π .
Let us now consider full ASP, where rule bodies involve negative literals. Assume there are n occurrences of not A in the body of rules of given program Π . To represent full RASP (and thus full ASP) we improve the transformation devised in Definition 3: Definition 5. Given ASP program Π , the corresponding Linear Logic RASP Theory ΣΠ is obtained by applying, in sequence, the following rewritings.
– For each atom A occurring negated in rules of Π , standardize apart each of its negated occurrences by replacing not A with not A j:1, in the j-th rule. Being not A j1 :1, . . ., not A jn :1 all the occurrences introduced in this manner, add the (linear) fact not A:n to the translation of Π . – For each rule A ← B1, . . . , B` of Π . Let such rule be the j-th one; rewrite it as A ← B1, . . . , B`, not A j:n.
Let us denote by not Ak1 :n, . . ., not Aks :n all the atoms introduced in this manner.4 – Apply the rewriting indicated in Definition 3 to the result of the previous steps. – Finally, for each linear fact not A:n added to ΣΠ (cf., the first two steps), also add the &-Horn implications to the translation of Π : (not A:n — ◦ not Ak1 :n) & . . . & (not A:n — ◦ not Aks :n) & (not A:n — ◦ not A j1 :1 ⊗ . . . ⊗ not A jn :1) 4 In case identical atoms would be introduced in the body in consequence of different steps of the translation, e.g., not Ak:1 and not Ak:1 might occur in the same rule if n equals 1 in the first step andnot A already appeared in the ASP rule body, then further standardize apart these occurrences, e.g., as not Ak1:1 and not Ak2:1.
The intuitive meaning behind this translation is that the assumption not A is made available to every rule that intends to adopt it, unless A itself is provable. In which case the assumption becomes totally unavailable (as proving A consumes the full available quantity of the “resource” not A).
The transformation of Definitions 3 and 5 is clearly polynomial, as we add: (i) a new conjunct in the body (not A if the rule head is A) and new elements (r-copies) in the head of rules ; (ii) one &-Horn implication for each A occurring in the head of some rule; (iii) one linear implication for each atom defined via several rules; (iv) one &-Horn implication for each A occurring negatively in the body of some rule. Hence, we have: Theorem 2. Let Π be an ASP program, and ΣΠ the corresponding Linear Logic RASP Theory, obtained according to Definitions 3 and 5. Let M = {A1, . . . , An} be an answer set for Π . Then, A1 ⊗ . . . ⊗ An is a maximal tensor conjunction provable from ΣΠ .
Note that the reverse result does not necessarily hold, because there are maximal
tensor conjunctions that are not answer sets but are provable from ΣΠ . This is due (as
discussed in [
It is interesting to notice that the linear logic formulation we summarized in the previous section prevents contradictions. Consider for example the program Π1 = {p ← not p.}. It is transformed into: not p11:1 ⊗ not p12:1 — ◦ p, not p:1, (not p:1 — ◦ not p11:1) & (not p:1 — ◦ not p12:1)
In the first rule, one occurrence ofnot p corresponds to the one originally present, the other one has been added as for proving p it is necessary to “absorb” the whole available quantity of not p (consider n = 1 in Definition 5). We can in fact verify that the singleton tensor conjunction p is by no means provable: in fact, it would require two units of not p, while just one is available. This does not lead to inconsistency, but simply to the impossibility to prove p.
Consider again program Π = {a ← not b. b ← not c. c ← not a.} which is an “odd cycle” involving three atoms. In our formulation, ΣΠ is the following: not a1:1 ⊗ not b1:1 — ◦ a not c2:1 ⊗ not b2:1 — ◦ b not a3:1 ⊗ not c3:1 — ◦ c not a:1 not b:1 not c:1 (not a:1 — ◦ not a1:1) & (not a:1 — ◦ not a3:1) (not b:1 — ◦ not b1:1) & (not b:1 — ◦ not b2:1) (not c:1 — ◦ not c2:1) & (not c:1 — ◦ not c3:1)
From this linear logic theory we can prove the three maximal tensor conjunctions, namely, a, b and c. Assume, in fact, to try to prove a (the cases of b and c are of course analogous). Proving a uses resources not a1:1 and not b1:1. Therefore, after proving a, b cannot be proved because its own negation (i.e., not b2:1) is not available: in fact, the &-Horn implication related to b generates (indifferently) only one of the two items, and has already been requested to produce not b1:1 for proving a. In turn, c cannot be proved because not a3:1 is not available, as the &-Horn implication related to a generates (indifferently) only one of the two items, and has already been requested to produce not a1:1 for proving a. Then, ΣΠ behaves analogously to the GL-reduct as far as c is concerned, being not a unavailable once a has been proved. But it behaves in a more uniform way on b, in the sense that once not b has been used to prove a, it is no longer possible to prove b.
This means that the 3-atoms odd cycles is interpreted as an exclusive disjunction, exactly like the 2-atoms even cycle (such as {q ← not p. p ← not q.}) in AS. Therefore, in the generate-and-test perspective which is at the basis of the ASP programming methodology, our new view provides a new mean of easily generating the search space.
The ternary cycle has many well-known interpretations in terms of knowledge representation, among which the following is an example: {beach ← not mountain. mountain ← not travel.
travel ← not beach.}
In our approach we would have exactly one of (indifferently) beach, mountain, or travel.
Similarly for the program {work ← not tired. tired ← not sleep. sleep ← not work.}.
Note that, in answer set programming, for defining the exclusive disjunction of three
atoms one has to resort to the extremal program [
There are other semantic approaches to managing odd cycles, such as for instance
[
Below we provide a variation of the answer set semantics that defines resourcebased answer sets.
Definition 6. Let Π be a program and I a minimal model of Π . I is called a Π -based minimal model iff ∀A ∈ I, there exists a rule in Π with head A and positive body C1, . . . ,Cm, m ≥ 0, where {C1, . . . ,Cm} ⊆ I.
Definition 7. Let Π be a program. M is a resource-based answer set of Π iff M = ΓΠ (I), where I is a Π -based minimal model of Π .
By Definition 7, there is a resource-based answer set for each Π -based classical minimal model. It is clear that answer sets are among resource-based answer sets. In fact, as stated in Section 3 (Proposition 1), for any minimal model I it holds ΓΠ (I) ⊆ I: thus any answer set S, being a minimal model which is equal to ΓΠ (S), fits as a particular case in the above definition. Therefore, some of the resource-based answer sets ofΠ are classical models (coinciding with its answer sets), while the others are subsets of the remaining Π -based minimal models (if any). Non-empty resource-based answer sets still form an anti-chain w.r.t. set inclusion.
We call the new semantics RAS semantics (Resource-Based Answer Set semantics),
w.r.t. AS (Answer Set) semantics. Differently from answer sets, a (possibly empty)
resource-based answer set always exists. Complexity of RAS semantics is however
higher than complexity of AS semantics: in fact, [
The previous result about the relation with linear logic (Theorem 2) extends to the
new semantics. The proof, reported in [
It remains to be explained why the new definition models the intuition, and how
it applies to practical cases. In particular, given minimal model I of Π , it may be that
ΓΠ (I) ⊂ I, i.e., ΓΠ (I) is a proper subset of I and thus I is not an answer set, for only
one reason. For atom A to belong to a Π -based minimal model I, there exists some rule
in Π with head A. For A not to belong to ΓΠ (I), so that ΓΠ (I) ⊂ I, each of the rules
that could cause A to be in the model must have been canceled by step (1) of ΓΠ , as
they include literal not B in their body, B ∈ I. Atoms belonging to ΓΠ (I) are therefore
those atoms in I that can be derived without such contradictions. As widely discussed in
[
Regarding general odd cycles involving k atoms, of the form {a1 ← not a2. a2 ← not a3. . . . ak ← not a1.}, it is easy to see that each such cycle has k classical minimal Π -based models (it admits k classical minimal models, all of them Π -based as there are no positive conditions). Correspondingly, we obtain k resource-based answer sets, where we have Mi = {ai+d , with d even, 0 ≤ d < k − 1}. This fact can be verified by producing a translation into the corresponding Linear Logic RASP Theory analogous to the one performed above for unary and ternary cycles. Then, unfortunately, odd cycles no longer model disjunction if k > 3, similarly to even cycles, which do not model disjunction if k > 2.
In resource-based answer set semantics, there are no inconsistent programs.
Nevertheless, the new semantics is useful in knowledge representation not just to fix
inconsistencies: rather, it depicts a more general scenario in many reasonable examples.
Consider for instance the variation of the above program (inspired to examples proposed
in [
forgot renew ← not passport ok.
This program has answer set M1 = {forgot renew, mountain}, as passport ok being false forces travel to be false, which in turn makes mountain true. The answer set semantics cannot cope with the case of the passport being ok, which is in fact excluded as this option determines no answer set. Instead, in resource-based answer set semantics we have, in addition to M1, three other answer sets stating that, if the passport is ok, any choice is possible, namely we have M2 = {passport ok, mountain}, M3 = {passport ok, beach}, and M4 = {passport ok, travel}. We may notice that the semantics is still a bit strong on this example on the side of the answer set, as one would say that not having passport ok prevents traveling, but any other choice should be possible, while instead the mountain choice is forced.
A better formalization of the above example would be by means of the plain odd cycle, plus the even cycle concerning passport, plus the constraint
← not passport ok, travel.
In the next section we will discuss how to introduce such a constraint, as a unary odd cycle is no longer usable to this purpose. 6
In resource-based answer set semantics, constraints cannot be modeled in terms of odd
cycles. Therefore, they have to be modeled explicitly. In particular, let assume a
constraint C to be of the form ← E1, . . . , En. where the Eis are atoms5. This is with no loss
of generality, as a constraint such as, for instance, ← A, not B. can be reformulated as
the program fragment ← A, B0. B0 ← not B. Thus, an overall program ΠO can be seen
as composed of answer set program Π plus a set {C1, . . . , Cv} of constraints, and,
possibly, an auxiliary program ΠC , so that constraints can be defined on atoms belonging
to either Π or ΠC . We assume however that ΠC is stratified (i.e., it contains no cycles,
cf. e.g., [
hyperthyroidism.} plus the following ΠC :
{unhealthy ← beach, hyperthyroidism.} plus the constraint ← unhealthy.
hyperthyroidism}, and {travel, hyperthyroidism}, while {beach, hyperthyroidism, unhealthy} is excluded by the constraint. We now proceed to the formal definition. Definition 8. An Answer Set Theory T is a couple hΠO , Constri, with ΠO = Π ∪ ΠC , where ΠC is a top program for Π , and where Constr is a set {C1, . . . , Cv}, v ≥ 0, of constraints.
Definition 9. Given Answer Set Theory T = hΠO , Constri, a resource-based Answer Set M for Π fulfills the constraints in Constr iff the answer set program Π 0 is consistent (in the sense of traditional answer set semantics), where Π 0 is obtained from ΠC by adding all atoms in M as facts, and all constraints in Constr as rules.
Definition 10. A Resource-based Answer Set M of Answer Set Theory T = hΠO , Constri is a resource-based answer set for Π that fulfills all constraints in Constr.
It is easy to see that, in order to check that resource-based Answer Set M for Π
fulfills the constraints, one can check consistency ofΠ 0 in a simple way, by: (i) computing
(in polynomial time, cf., e.g., [
The partition of ΠO into Π and ΠC is not strictly necessary in the present context.
In fact, one might simply check the constraints on Π ∪ ΠC . However, we choose to
introduce the distinction because we believe that it may have a significance in terms
of knowledge representation and elaboration-tolerance, in the sense of [
For the sake of completeness, it may be interesting to illustrate the linear logic formalization of the full approach. To this aim, we have to resort to linear logic negation. A constraint C = ← E1, . . . , En. can in fact be represented in linear logic as C L = E1⊥ O . . . O En⊥ where O is the multiplicative disjunction, and ⊥ is linear logic negation, A⊥ meaning “there is no proof for A”. 6
sets should be matched against the constraints. Formally: Definition 11. Given resource-based answer set M = {A1, . . . , An} for ΠO , M is a resource-answer set for answer set theory T = hΠO , Constri where Constr = {C1, . . . , Cv} iff tensor conjunction A1 ⊗ . . . ⊗ An ⊗ C1L⊗ . . . ⊗ CvL is provable from ΣΠO .
Notice that each constraint is provable whenever at least one of its disjuncts is not one of the Ai’s. Then, in terms of equivalence between the logic programming and linear logic formulation, nothing really changes w.r.t. Theorem 3. 7
In this paper, we have proposed an extension of the answer set semantics where ternary odd cycles are understood as exclusive disjunctions, similarly to binary even cycles. This extension stems from the interpretation of an answer set program as a linear logic theory, where default negation is considered to be a resource. The practical advantage is that there is more freedom in defining a search space, where constraints must however be defined in a separate “module” to be added to given answer set program.
Concerning implementation, which is of course a main future issue for this research, answer set solvers based on SAT appear to be good candidates for extension to the new setting. In fact, apart from checking for minimality of models (which is the part responsible for the additional complexity), they do not seem to need substantial modifications in order to cope with the new semantics, that thus might in principle be easily and quickly implemented.