For practical applications, the use of top-down query-driven proofprocedures is convenient for an efficient use and computation of answers using Logic Programs as knowledge bases. Additionally, abductive reasoning on demand is intrinsically a top-down search method. A 2-valued semantics for Normal Logic Programs (NLPs) allowing for top-down query-solving is thus highly desirable, but the Stable Models semantics (SM) does not allow it, for lack of the relevance property. To overcome this limitation we introduced in [24], and review here, a new 2-valued semantics for NLPs - the Layer Supported Models semantics - which conservatively extends the SM semantics, enjoys relevance and cumulativity, guarantees model existence, and respects the Well-Founded Model. In this paper we also exhibit a transformation, TR, from one propositional NLP into another, whose Layer Supported Models are precisely the Stable Models of the transform, which can then be computed by extant Stable Model implementations, providing a tool for the immediate generalized use of the new semantics and its applications. In the context of abduction in Logic Programs, when finding an abductive solution for a query, one may want to check too whether some other literals become true (or false) as a consequence, strictly within the abductive solution found, that is without performing additional abductions, and without having to produce a complete model to do so. That is, such consequence literals may consume, but not produce, the abduced literals of the solution. To accomplish this mechanism, we present the concept of Inspection Point in Abductive Logic Programs, and show, by means of examples, how one can employ it to investigate side-effects of interest (the inspection points) in order to help choose among abductive solutions.
The semantics of Stable Models (SM) [14] is a cornerstone for the definition of some of
the most important results in logic programming of the past two decades, providing an
increase in logic programming declarativity and a new paradigm for program
evaluation. When we need to know the 2-valued truth value of all the literals in a logic program
for the problem we are modeling and solving, the only solution is to produce complete
models. Depending on the intended semantics, in such cases, tools like SModels [19] or
DLV [
SM semantics does not allow for top-down query-solving precisely because it does not enjoy the relevance property — and moreover, does not guarantee the existence of a model. Furthermore, frequently there is no need to compute whole models, like its implementations do, but just the partial models that sustain the answer to a query. Relevance would ensure these could be extended to whole models.
Furthermore, with SM semantics, in an abductive reasoning situation, computing the whole model entails pronouncement about every abducible whether or not it is relevant to the problem at hand, and subsequently filtering the irrelevant ones. When we just want to find an existential answer to a query, we either compute a whole model and check if it entails the query (the way SM semantics does), or, if the underlying semantics we use enjoys the relevance property — which SM semantics do not — we can simply use a top-down proof-procedure (à la Prolog), and abduce by need. In this second case, the user does not pay the price of computing a whole model, nor the price of abducing all possible abducibles or their negations, and then filtering irrelevant ones, because the only abducibles considered will be those needed to answer the query.
To overcome these limitations we developed in [24] (reviewed here) a new 2-valued
semantics for NLPs — the Layer Supported Models (LSM) — which conservatively
extends the SMs, enjoys relevance and cumulativity, guarantees model existence, and
respects the Well-Founded Model (WFM) [
The LSM semantics builds upon the foundational step of the Layered Models semantics presented in [27] by imposing a layered support requirement resulting in WFM consonance. In [27], neither layered support nor WFM respect are required. Intuitively, a program is conceptually partitioned into “layers” which are subsets of its rules, possibly involved in mutual loops. An atom is considered true if there is some rule for it at some layer, where all the literals in its body which are supported by rules of lower layers are also true. Otherwise that conclusion is false. That is, a rule in a layer must, to be usable, have the support of rules in the layers below.
Although Stable Models is a great semantics with a simple definition, it nevertheless
fails to provide semantics for all normal programs. LSM coincides with Stable Models
whenever the latter is defined (no odd loops ou infinite chains), — [
The core reason SM semantics fails to guarantee model existence for every NLP is that the stability condition it imposes on models is impossible to be complied with by Odd Loops Over Negation (OLONs). An OLON is a loop with an odd number of default negations in its circular call dependency path. In fact, the SM semantics community uses that inability as a means to impose Integrity Constraints (ICs), such as a where the OLON over a prevents X from being true in any model.
The LSM semantics provides a semantics to all NLPs. In the a not a; X example above, whenever X is true, the only LSM is fa; Xg. For LSM semantics OLONs are not ICs. ICs are implemented with rules for reserved atom f alsum, of the form f alsum X, where X is the body of the IC we wish to prevent being true. This does not prevent f alsum from being in some models. From a theoretical standpoint this means that the LSM semantics does not include an IC compliance enforcement mechanism. ICs must be dealt with in two possible ways: either by 1) a syntactic post-processing step, as a “test phase” after the model generation “generate phase”; or by 2) embedding the IC compliance in a query-driven (partial) model computation, where such method can be a top-down query-solving one a la Prolog, since the LSM semantics enjoys relevance. In this second case, the user must conjoin query goals with not f alsum. If inconsistency examination is desired, like in the 1) case above, models including f alsum can be discarded a posteriori. This is how LSM semantics separates OLON semantics from IC compliance.
After notation and background definitions, we summarize the formal definition of LSM semantics and its properties. Thereafter, in a section that may be skipped without loss of continuity, we present a program transformation, TR, from one propositional (or ground) NLP into another, whose Layer Supported Models are precisely the Stable Models of the transform, which can be computed by extant Stable Model implementations, which also require grounding of programs. TR’s space and time complexities are then examined. TR can be used to answer queries but is also of theoretical interest, for it may be used to prove properties of programs, say. Moreover, TR can be employed in combination with the top-down query procedure of XSB-Prolog, and be applied just to the residual program corresponding to a query (in compliance with the relevance property of Layer Supported Models). The XSB-XASP interface then allows the program transform to be sent for Smodels for 2-valued evaluation. Thus, for existential query answering there is no need to compute total models, but just the partial models that sustain the answer to the query, or one might simply know a model exists without producing it; relevance ensures these can be extended to total models.
In its specific implementation section we indicate how TR can be employed, in combination with the top-down query procedure of XSB-Prolog, it being sufficient to apply it solely to the residual program corresponding to a query (in compliance with the relevance property of Layer Supported Model ). The XSB-XASP interface allows the program transform to be sent for Smodels for 2-valued evaluation. Implementation details and attending algorithms can be found in [25].
Next, issues of reasoning with logic programs are addressed in section 7 where, in particular, we look at abductive reasoning and the nature of backward and forward chaining in their relationship to the issues of query answering and of side-effects examination within an abductive framework. In section 8 we then introduce inspection points to address such issues, illustrate their need and use with examples, and provide for them a declarative semantics. The touchstone of enabling inspection points can be construed as meta-abduction, by (meta-)abducing an “abduction" to check (i.e. to passively verify) that a certain concrete abduction is indeed adopted in a purported abductive solution. In section 8.2 we surmise their implementation, the latter’s workings being fully given and exemplified in [23]. We have implemented inspection points on top of already existing 3- and 2-valued abduction solving systems — ABDUAL and XSB-XASP — in a way that can be adopted by other systems too.
Our semantics can easily be extended to deal with Disjunctive Logic Programs
(DisjLPs) and Extended Logic Programs (ELPs, including explicit negation), by means of
the shifting rule and other well-known program transformations [
H B1; : : : ; Bn; not C1; : : : ; not Cm where H, the Bi and the Cj are atoms. We call H the head of the rule — also denoted by head(r). And body(r) denotes the set fB1; : : : ; Bn; not C1; : : : ; not Cmg of all the literals in the body of r. Throughout this paper we will use ‘not ’ to denote default negation. When the body of the rule is empty, we say the head of rule is a fact and we write the rule just as H. A Logic Program (LP for short) P is a (possibly infinite) set of ground Logic Rules of the form in Definition 1. In this paper we focus mainly on NLPs, those whose heads of rules are positive literals, i.e., simple atoms; and there is default negation just in the bodies of the rules. Hence, when we write simply “program” or “logic program” we mean an NLP. 3
The well-known notion of stratification of LPs has been studied and used for decades
now. But the common notion of stratification does not cover all LPs, i.e., there are some
LPs which are non-stratified. The usual syntactic notions of dependency are mainly
focused on atoms. They are based on a dependency graph induced by the rules of the
program. Useful these notions might be, for our purposes they are insufficient as they
leave out important structural information about the call-graph of P . To cover that
information we also define below the notion of a rule’s dependency. Indeed, layering puts
rules in layers, not atoms. An atom B directly depends on atom A in P iff there is at
least one rule with head B and with A or not A in the body. An atom’s dependency is
just the transitive closure of the atom’s direct dependency. A rule directly depends on
atom B iff any of B or not B is in its body. A rule’s dependency is just the transitive
closure of the rule’s direct dependency. The Relevant part of P for some atom A,
represented by RelP (A), is the subset of rules of P with head A plus the set of rules of P
whose heads the atom A depends on, cf. [
Definition 2. Parts of the body of a rule. Let r = H B1; : : : ; Bn; not C1; : : : ; not Cm be a rule of P . Then, rl = fBi; not Cj : Bi depends on H ^ Cj depends on Hg. Also, rB = fBi : Bi 2 (body(r) n rl)g, and rC = fCj : not Cj 2 (body(r) n rl)g.
literals: its result is the highest layer number of all the rules for all the literals in the set, or zero if the set is empty.
function L=1 is just any function defined over the rules of P 0, where P 0 is obtained from
assigning each rule r 2 P 0 a positive integer, such that: – L(r) = 0 if f alsum 2 body(r), otherwise – L(r) max(HighLayer(rl); HighLayer(rB); (HighLayer(rC ) + 1))
r having L(r) = i, i.e., those which depend only on the rules in the same layer or layers below it.
This notion of layering does not correspond to any level-mapping [16], since the later is
defined over atoms, and the former is defined over rules. Also, due to the definition of
dependency, layering does not coincide with stratification [
Amongst the several possible layerings of a program P we can always find the least one, i.e., the layering with least number of layers and where the integers of the layers are smallest. In the remainder of the paper when referring to the program’s layering we mean such least layering (easily seen to be unique).
Example 1. Layering example. Consider the following program P , depicted along with the layer numbers for its least layering: c d y x a not d; not y; not a not c not x not x f alsum b b not x
Layer 3 Layer 2 Layer 1 Layer 0
Atom a has no rules so its now created unique rule a f alsum is placed in Layer 0. Atom b has a fact rule rb1 : its body is empty, and therefore all HighLayer(rbl1 ), HighLayer(rbB1 ), and HighLayer(rbC1 ) are 0 (zero). Hence, L(rb1 ) = max(0; 0; (0 + 1)) = max(0; 0; 1) = 1, where rb1 is the fact rule for b, placed in Layer 1.
The unique rule for x, rx is also placed in Layer 1 in the least layering of P because HighLayer(rxl) = L(rx), HighLayer(rxB) = 0, and HighLayer(rxC ) = 0. So, L(rx) = max(L(rx); 0; (0 + 1)) = max(L(rx); 0; 1) = 1, in the least layering.
The unique rule for c, rc is placed in Layer 3 because HighLayer(rcC ) = 2, HighLayer(rcB) = 0, and HighLayer(rcl) = HighLayer(rd) = 3. By the same token, rd is placed in the same Layer 3. Both rb2 and ry are placed in Layer 2.
This program has two LSMs: fb; c; xg, and fb; d; xg.
The complexity of computing the Layering of a given ground NLP is conjectured to be in the same order as that of the Tarjan’s Strongly Connected Components detection Algorithm, which is known to be linear in the number of nodes and edges on the dependency graph: O(jN j + jEj). 4
The Layer Supported Models semantics we now present is the result of the two new notions we introduced: the layering, formally introduced in section 3, which is a generalization of stratification; and the layered support, as a generalization of classical support. These two notions are the means to provide the desired 2-valued semantics which respects the WFM, as we will see below.
An interpretation M of P is classically supported iff every atom a of M is classically supported in M , i.e., all the literals in the body of some rule for a are true under M in order for a to be supported under M .
Definition 5. Layer Supported interpretation. An interpretation M of P is layer supported iff every atom a of M is layer supported in M , and this holds iff a has a rule r where all literals in (body(r) n rl) are true in M . Otherwise, it follows that a is false. Theorem 1. Classical Support implies Layered Support. Given an NLP P , an interpretation M , and an atom a such that a 2 M , if a is classically supported in M then a is also layer supported in M .
Proof. Trivial from the definitions of classical support and layered support. tu In programs without odd loops layered supported models are classically supported too. Example 2. Layered Unsupported Loop. Consider program P :
c not a a c; not b b
The only rule for b is in the first layer of P . Since it is a fact it is always true in the WFM. Knowing this, the body of the rule for a is false because unsupported (both classically and layered). Since it is the only rule for a, its truth value is false in the WFM, and, consequently, c is true in the WFM. This is the intuitively desirable semantics for P , which corresponds to its LSM semantics. LM and the LSM semantics differences reside both in their layering notion and the layered support requisite of Def. 5. In this example, if we used LM semantics, which does not exact layered support, there would be two models: LM1 = fb; ag and LM2 = fb; cg. fbg is the only minimal model for the first layer and there are two minimal model extensions for the second layer, as a is not necessarily false in the LM semantics because Def. 5 is not adopted. Lack of layered support lets LM semantics fail to comply with the WFM. Note that adding a rule like b a would not affect the semantics of the program, according to LSM. This is so because, such rule would be placed in the same layer with the rules for a and c, but leaving the fact rule b in the strictly lower layer.
Intuitively, the minimal layer supported models up to and including a given layer, respect the minimal layer supported models up to the layers preceding it. It follows trivially that layer supported models are minimal models, by definition. This ensures the truth assignment to atoms in loops in higher layers is consistent with the truth assignments in loops in lower layers and that these take precedence in their truth labeling. As a consequence of the layered support requirement, layer supported models of each layer comply with the WFM of the layers equal to or below it. Combination of the (merely syntactic) notion of layering and the (semantic) notion of layered support makes the LSM semantics.
81 i nM j i is a minimal layer supported model of [1 j i P j where M j i denotes the restriction of M to heads of rules in layers less or equal to i:
M j i M \ fhead(r) : L(r) ig
Example 3. Layer Supported Models semantics. Consider again the program from example 1. Its LS models are fb; c; xg, and fb; d; xg. According to LSM semantics b and x are true because they are in the intersection of all models. c and d are undefined, and a and y are false.
Layered support is a more general notion than that of perfect models [30], with similar structure. Perfect model semantics talks about “least models” rather than “minimal models” because in strata there can be no loops and so there is always a unique least model which is also the minimal one. Layers, as opposed to strata, may contain loops and thus there is not always a least model, so layers resort to minimal models, and these are guaranteed to exist (it is well known every NLP has minimal models).
The simple transformation step adding a rule of the form a f alsum for atoms a with no rules in P enforces compliance with the Closed World Assumption (CWA).
The principle used by LSMs to provide semantics to any NLP — whether with OLONs or not — is to accept all, and only, the minimal models that are layer supported, i.e., that respect the layers of the program. The principle used by SMs to provide semantics to only some NLPs is a “stability” (fixed-point) condition imposed on the SMs by the Gelfond-Lifschitz operator.
In [27] the authors present an example (7) where three alternative joint vacation solutions are found by the LM semantics, for a vacation problem modeled by an OLON. The solutions found actually coincide with those found by the LSM semantics. We recall now a syntactically similar example (from [29]) but with different intended semantics, and show how it can be attained in LSM by means of ICs.
Example 4. Working example [29].
tired not sleep sleep not work work not tired As in the example 7 of [27], the LSM semantics would provide three solutions for the above program: fwork; tiredg; fwork; sleepg; fsleep; tiredg. Although some (or even all!) of these solutions might be actually plausible in a real world case, they are not, in general, the intended semantics for this example. With the LSM semantics, the way to prune away some (or all) of these solutions is by means of ICs. For example, to eliminate the fwork; sleepg solution we would just need to add the IC f alsum work; sleep. Again, an IC compliance mechanism, such as conjoining not f alsum to the query, must be employed by the user in order to eliminate the undesired models. Example 5. Jurisprudential reasoning. A murder suspect not preventively detained is likely to destroy evidence, and in that case the suspect shall be preventively detained: likely_destroy_evidence(murder_suspect)
not preventively_detain(murder_suspect) preventively_detain(murder_suspect)
likely_destroy_evidence(murder_suspect)
There is no SM, and a single LSM = fpreventively_detain(murder_suspect)g. This jurisprudential reasoning is carried out without need for a murder_suspect to exist now. Should we wish, LSM’s cumulativity (cf. below) allows adding the model literal as a fact.
Example 6. Program with depth-unbound layering. A typical case of an infinitely
ground program (actually the only one with real theoretical interest, to the best of our
knowledge) was presented by François Fages in [
p(X) p(s(X)) p(X) not p(s(X)) Ground (layered) version of this program, assuming there only one constant 0 (zero): p(0) p(s(0)) p(s(s(0))) . . .
p(s(0)) p(s(s(0))) p(s(s(s(0)))) . . .
p(0) p(s(0)) p(s(s(0))) . . .
not p(s(0)) not p(s(s(0))) not p(s(s(s(0)))) . . .
The only layer supported model of this program is fp(0); p(s(0)); p(s(s(0))) : : :g or, in a non-ground form, fp(X)g. The theoretical interest of this program lies in that, although it has no OLONs it still has no SMs either because no rule is supported (under the usual notion of support), thereby showing there is a whole other class of NLPs to which the SMs semantics provides no model, due to the notion of support used. 5
Although the definition of the LSMs semantics is different from the LMs of [27], this
new refinement enjoys the desirable properties of the LMs semantics, namely:
guarantee of model existence, relevance, cumulativity, ([
Moreover, and this is the main contribution of the LSMs semantics, it respects the Well-Founded Model. It is not hard to recognize that the LM semantics [27] is the conservative generalization LSM semantics one obtains by removing the layered support condition on interpretations prescribed in Definition 6.
The complexity analysis of this semantics is left out of this paper. Nonetheless, a brief note is due. Model existence is guaranteed for every NLP, hence the complexity of finding if one LSM exists is trivial, when compared to SMs semantics. Brave reasoning — finding if there is any model of the program where some atom a is true — is an intrinsically NP-hard task from the computational complexity point of view. But since LSM semantics enjoys relevance, the computational scope of this task can be reduced to consider only RelP (a), instead of the whole P . From a practical standpoint, this can have a significant impact in the performance of concrete applications. Cautious reasoning (finding out if some atom a is in all models) in the LSM semantics should have the same computational complexity as in the SMs, i.e., coNP-complete. 5.1
Respect for the Well-Founded Model Definition 7. Interpretation M of P respects the WFM of P . An interpretation M respects the WFM of P iff M contains the set of all the true atoms of the WFM of P , and it contains no false atoms of the WFM of P .
M j i, respects the WFM of P i [ M j<i.
Theorem 2. Layer Supported Models respect the WFM. Let P be an NLP, and P i denote S1 j i P j , where P j is P ’s j layer. Each LSM M j i of P i, where M Proof. By hypothesis, each M j i is a full LSM of P i. Consider P 1. Any M j 1 contains the facts of P , and their direct positive consequences, since the rules for all of these are necessarily placed in the first layer in the least layering of P . Hence, M j 1 contains all the true atoms of the WFM of P 1. Layer 1 also contains whichever loops that do not depend on any other atoms besides those which are the heads of the rules forming the loop. Any such loops having no negative literals in the bodies are deterministic and, therefore, the heads of the rules forming the loop will be all true or all false in the WFM of P 1, depending on whether the bodies are fully supported by facts in the same layer, or not, and, in the latter case, if the rules are not involved in other types of loop making their heads undefined. In any case, an LSM of this layer will by necessity contain all the true atoms of the WFM of P 1. On the other hand, assume there is some atom b which is false in the WFM of P 1. b being false in the WFM means that either b has no rules or that every rule for b has an unsatisfiable body in P 1. In the first case, by definition 6 we know that b cannot be in any LSM. In the second case, every unsatisfiable body is necessarily unsupported, both classically and layered. Hence, b cannot be in any LSM of P 1. This means that any LSM contains no atoms false in the WFM of P 1, and, therefore, that they must respect the WFM of P 1.
By hypothesis M j i+1 is an LSM of P i+1 iff M j i+1 M j i, for some LSM M j i of P i, which means the LSMs M j i+1 of P i+1 are exactly the LSMs M j i+1 of P i+1 [ M j i. Adding the M j i atoms as facts imposes them as true in the WFM of P i+1 [ M j i. The then deterministically true consequences of layer i + 1 — the true atoms of the WFM of P i+1 [ M j i — become necessarily present in every minimal model of P i+1 [ M j i, and therefore in its every LSM M j i+1. On the other hand, every atom b false in the WFM of P i+1 [ M j i has now unsatisfiable bodies in all its rules (up to this layer i+1). Hence, b cannot be in any LSM of P i+1 [M j i. Therefore, every M j i+1 respects the WFM of P i+1 [ M j i. Hence, more generally, every M j i respects the WFM of P i [ M j<i tu 5.2
Other Comparisons We next argue informally that the LSMs and the Revised Stable Models (RSMs) defined in [21] are the same. The equivalence is rather immediate. Take Definitions 2 and 3 of [21] characterizing the RSMs: Definition 8. Sustainable Set (Definition 2 in [21]). Intuitively, we say a set S is sustainable in P iff any atom a 2 S does not go against the well-founded consequences of the remaining atoms in S, whenever, S n fag itself is a sustainable set. The empty set by definition is sustainable. Not going against means that atom a cannot be false in the WFM of P [ S n fag, i.e., a is either true or undefined. That is, it belongs to set P [Snfag(W F M (P [ S n fag)). Formally, we say S is sustainable iff 8a2S S n fag is sustainable ) a 2 P [Snfag(W F M (P [ S n fag)) where P (I) is just the Gelfond-Lifschitz program division of P by interpretation I. Definition 9. Revised Stable Models and Semantics (Definition 3 in [21]). Let RAAP (M ) M n P (M ). M is a Revised Stable Model of a NLP P , iff: – M is a minimal classical model, with not interpreted as classical negation, and – 9 2 such that P (M ) RAAP (M ) – RAAP (M ) is sustainable
The first item goes without saying for both semantics. For the third item, it is apparent that sustainable models respect the WFS as required of LSM models; vice-versa, LSM models are sustainable models. Finally, for the 2nd item, consider its justification provided after Def. 3 of [21]. It should be clear, after due consideration, that the 2nd item holds for LSMs and, vice-versa, that RSMs, because they comply with it, will comply with the minimal models at each LSM layer, which always resolve the odd loops that may be present in it.
Only recently, we became aware of the work of Osorio et. al [20]. Their approach, couched in argumentation terms, addresses the same semantic concerns as our own, apparently with similar results for the case of finite propositional normal programs, though the paper does not produce a proof of respecting the WFS. In [22] we also address the same concerns in argumentation semantics terms having providing the Approved Models semantics. The latter can be made to respect the WFS only if desired, by means of an appropriate condition, and so appears to be more general than that of [20]. Moreover, Approved Models is conjectured to result, in that case, in a semantics equivalent to the RSMs [21] and the LSMs.
The program transformation we now define (which can be skipped without loss of
continuity) provides a syntactical means of generating a program P 0 from an original
program P , such that the SMs of P 0 coincide with the LSMs of P . It engenders an expedite
means of computing LSMs using currently available tools like Smodels [19] and DLV
[
To produce P 0 from P we need a means to detect OLONs. The OLON detection mechanism we employ is a variant of Tarjan’s Strongly Connected Component (SCC) detection algorithm [34], because OLONs are just SCCs which happen to have an odd number of default negations along its edges. Moreover, when an OLON is detected, we need another mechanism to change its rules, that is to produce and add new rules to the program, which make sure the atoms a in the OLON now have “stable” rules which do not depend on any OLON. We say such mechanism is an “OLON-solving” one. Trivial OLONs, i.e. with length 1 like that in the Introduction’s example (a not a; X), are “solved” simply by removing the not a from the body of the rule. General OLONs, i.e. with length 3, have more complex (non-deterministic) solutions, described below. Minimal Models of OLONs In general, an OLON has the form
R1 = 1 not 2; 1 R2 = 2 not 3; 2 . . .
Rn = n not 1; n where all the i are atoms, and the j are arbitrary conjunction of literals which we refer to as “contexts”. Assuming any i true alone in some model suffices to satisfy any two rules of the OLON: one by rendering the head true and the other by rendering the body false.
i 1 i; i 1, and i i+1; i A minimal set of such i is what is needed to have a minimal model for the OLON. Since the number of rules n in OLON is odd we know that n2 1 atoms satisfy n 1 rules of OLON. So, n2 1 + 1 = n+21 atoms satisfy all n rules of OLON, and that is the minimal number of i atoms which are necessary to satisfy all the OLON’s rules. This means that the remaining n n+21 = n2 1 atoms i must be false in the model in order for it to be minimal.
Taking a closer look at the OLON rules we see that 2 satisfies both the first and second rules; also 4 satisfies the third and fourth rules, and so on. So the set f 2; 4; 6; : : : ; n 1g satisfies all rules in OLON except the last one. Adding 1 to this set, since 1 satisfies the last rule, we get one possible minimal model for OLON: MOLON = f 1; 2; 4; 6; : : : ; n 1g. Every atom in MOLON satisfies 2 rules of OLON alone, except 1, the last atom added. 1 satisfies alone only the last rule of OLON. The first rule of OLON — 1 not 2; 1 — despite being satisfied by 1, was already satisfied by 2. In this case, we call 1 the top literal of the OLON under M . The other Minimal Models of the OLON can be found in this manner simply by starting with 3, or 4, or any other i as we did here with 2 as an example. Consider the MOLON = f 1; 2; 4; 6; : : : ; n 1g. Since i+1 2 body(Ri) for every i < n, and 1 2 body(Rn); under MOLON all the R1; R3; R5; : : : ; Rn will have their bodies false. Likewise, all the R2; R4; R6; : : : ; Rn 1 will have their bodies true under MOLON . This means that all 2; 4; 6; : : : ; n 1 will have classically supported bodies (all body literals true), namely via rules R2; R4; R6; : : : ; Rn 1, but not 1 — which has only layered support (all body literals of strictly lower layers true). “Solving an OLON” corresponds to adding a new rule which provides classical support for 1. Since this new rule must preserve the semantics of the rest of P , its body will contain only the conjunction of all the “context” j , plus the negation of the remaining 3; 5; 7; : : : ; n which were already considered false in the minimal model at hand.
These mechanisms can be seen at work in lines 2.10, 2.15, and 2.16 of the Transform Literal algorithm below.
Definition 10. Top-down program transformation.
input : A program P output: A transformed program P’
Algorithm 1: TR Program Transformation
individual atom of P . The Transform Literal algorithm implements a top-down, ruledirected, call-graph traversal variation of Tarjan’s SCC detection mechanism. Moreover, when it encounters an OLON (line 2.9 of the algorithm), it creates (lines 2.13–
input : An literal l output: A partial transformed program Pa’ 2.1 previous context =context 2.2 Pa’ =P 2.3 atom =atom a of literal l; //removing the eventual not 2.4 if a has been visited then 2.5 if a or not a is in the stack then 2.6 scc root indx =lowest stack index where a or not a can be found 2.7 nots seq = sequence of neg. lits from (scc root indx +1) to top indx 2.8 loop length = length of nots seq 2.9 if loop length is odd then # nots in body = (loop length 1)
2 foreach ‘not x’ in nots seq do idx = index of not x in nots seq newbody = context for i=1 to # nots in body do newbody = newbody [
fnots seq ((idx + 2 i) mod loop length )g
Algorithm 2: Transform Literal context is true, but also only when that head is not classically supported, though being layered supported under the minimal model of the OLON it is part of. In the worst case, the whole P is a set of intricate OLONs. In such case there are exponentially many combinations of literals of P forming all the possible contexts, and for each of them TR adds a new rule. Hence, the complexity of TR is conjectured to be exponential in the number of atoms of P . Since the main purpose of this transformation is to be used for top-down query-solving, only the relevant atoms for the query are explored and their respective new rules produced. This way, the transformation can be applied on a “by need” basis.
Example 7. Solving OLONs. Consider this program, coinciding with its residual: a not a; b b c c not b; not a
Solving a query for a, we use its rule and immediately detect the OLON on a. The leaf not a is removed; the rest of the body fbg is kept as the Context under which the OLON on a is “active” — if b were to be false there would be no need to solve the OLON on a’s rule. After all OLONs have been solved, we use the Contexts to create new rules that preserve the meaning of the original ones, except the new ones do not now depend on OLONs. The current Context for a is now just fbg instead of the original fnot a; bg.
Solving a query for b, we go on to solve c — fcg being b’s current Context. Solving c we find leaf not b. We remove c from b’s Context, and add c’s body fnot b; not ag to it. The OLON on b is detected and the not b is removed from b’s Context, which finally is just fnot ag. As can be seen so far, updating Contexts is similar to performing an unfolding plus OLON detection and resolution by removing the dependency on the OLON. The new rule for b has final Context fnot ag for body. I.e., the new rule for b is b not a. Next, continuing a’s final Context calculation, we remove b from a’s Context and add fnot ag to it. This additional OLON is detected and not a is removed from a’s Context, now empty. Since we already exhausted a’s dependency call-graph, the final body for the new rule for a is empty: a will be added as a fact. Moreover, a new rule for b will be added: b not a. The final transformed program is: a not a; b a b c b not a c not b; not a it has only one SM = fag the only LSM of the program. Mark layering is respected when solving OLONs: a’s final rule depends on the answer to b’s final rule. Example 8. Solving OLONs (2). Consider this program, coinciding with its residual: a not b; x b not c; y c not a; z x y z Solving a query for a we push it onto the stack, and take its rule a not b; x. We go on for literal not b and consider the rest of the body fxg as the current Context under which the OLON on a is “active”. Push not b onto the stack and take the rule for b. We go on to solve not c, and add the y to the current Context which now becomes fx; yg. Once more, push not c onto the stack, take c’s rule c not a; z, go on to solve not a and add z to the current Context which is now fx; y; zg. When we now push not a onto the stack, the OLON is detected and it “solving” begins. Three rules are created and added to the program a not c; x; y; z, b not a; x; y; z, and c not b; x; y; z. Together with the original program’s rules they render “stable” the originally “non-stable” LSM fa; b; x; y; zg, fb; c; x; y; zg, and fa; c; x; y; zg. The final transformed program is: a a not b; x not c; x; y; z b not c; y b
c not a; z
not a; x; y; z
x
c
6.2 Implementing the TR transformation
The XSB Prolog system1 is one of the most sophisticated, powerful, efficient and
versatile implementations, with a focus on execution efficiency and interaction with external
systems, implementing program evaluation following the WFS for NLPs. The XASP
interface [
In our implementation, detailed below, we use XASP to compute the query relevant residual program on demand. When the TR transformation is applied to it, the resulting program is sent to Smodels for computation of stable models of the relevant sub-program provided by the residue, which are then returned to the XSB-XASP side. Residual Program After launching a query in a top-down fashion we must obtain the relevant residual part of the program for the query. This is achieved in XSB Prolog using the get_residual/2 predicate. According to the XSB Prolog’s manual “ the predicate get_residual/2 unifies its first argument with a tabled subgoal and its second argument with the (possibly empty) delay list of that subgoal. The truth of the subgoal is taken to be conditional on the truth of the elements in the delay list”. The delay list is the list of literals whose truth value could not be determined to be true nor false, i.e., their truth value is undefined in the WFM of the program.
It is possible to obtain the residual clause of a solution for a query literal, and in turn the residual clauses for the literals in its body, and so on. This way we can reconstruct the complete relevant residual part of the KB for the literal — we call this a residual program or reduct for that solution to the query.
More than one such residual program can be obtained for the query, on backtracking. Each reduct consists only of partially evaluated rules, with respect to the WFM, whose heads are atoms relevant for the initial query literal, and whose bodies are just the residual part of the bodies of the original KB’s rules. This way, not only do we get just the relevant part of the KB for the literal, we also get precisely the part of those rules bodies still undefined, i.e., those that are involved in Loops Over Negation. 1 XSB-Prolog and Smodels are freely available, at: http://xsb.sourceforge.net and http://www.tcs.hut.fi/Software/smodels.
Dealing with the Query and Integrity Constraints ICs are written as just f alsum IC_Body. An Smodels IC preventing f alsum from being true (:- falsum) is enforced whenever a transformed program is sent to Smodels. Another two rules are added to the Smodels clause store through XASP: one creates an auxiliary rule for the initially posed query; with the form: lsmGoal :- Query, where Query is the query conjunct posed by the user. The second rule just prevents Smodels from having any model where the lsmGoal does not hold, having the form: :- not lsmGoal.
The XSB Prolog source code for the meta-interpreter, based on this program transformation, is available at http://centria.di.fct.unl.pt/ amp/software.html 7
Logic Programs have been used for a few decades now in knowledge representation and reasoning. Amongst the most common kinds of reasoning performed using them, we can find deduction, induction and abduction. When query answering, if we know that the underlying semantics is relevant, i.e. guarantees it is enough to use only the rules relevant to the query (those in its call-graph) to assess its truthfulness, then we need not compute a whole model in order to find an answer to our query: it suffices to use just the call-graph relevant part of the program. This way of top-down finding a solution to a query, dubbed “backward chaining”, is possible only when the underlying semantics is relevant in the above sense, because the existence of a full model is guaranteed.
Currently, the standard 2-valued semantics used by the logic programming
community is Stable Models [14]. It’s properties are well known and there are efficient
implementations (such as DLV and SModels [
When performing abductive reasoning, we want to find, by need only (via backward chaining), one possible set of conditions (abductive literals of the program to be assumed either true or false) sufficient to entail our query. However, sometimes we also want to know which are (some of) the consequences (side-effects, so to speak) of such conditions. I.e., we want to know the truth value of some other literals, not part of the query’s call graph, whose truth-value may be determined by the abductive conditions found. In some cases, we might be interested in knowing every possible side-effect — the truth-value of every literal in a complete model satisfying the query and ICs. In other situations though, our focus is only in some specific side-effects of abductions performed.
In our approach, the side-effects of interest are explicitly indicated by the user by
wrapping the corresponding goals within reserved construct inspect=1. It is
advantageous, from a computational point of view, to be able to compute only the truth-value
of the important side-effects instead of the whole model, so as not to waste precious
time and computational resources. This is possible whenever the underlying semantics
guarantees model existence, and enjoys relevance.
Abduction, or inference to the best explanation, is a reasoning method whereby one
chooses the hypotheses that would, if true, best explain the observed evidence. In LPs,
abductive hypotheses (or abducibles) are named literals of the program which have no
rules. They can be considered true or false for the purpose of answering a query.
Abduction in LPs ([
Because they do not depend on any other literal in the program, abducibles can be modeled in a Logic Program system without specific abduction mechanisms by including for each abducible an even loop over default negation, e.g., abducible not neg_abducible: neg_abducible not abducible: where neg_abducible is a new abducible atom, representing the (abducible) negation of the abducible. This way, under the SM semantics, a program may have models where some abducible is true and another where it is false, i.e. neg_abducible is true. If there are n abducibles in the program, there will be 2n models corresponding to all the possible combinations of true and false for each. Under the WFS without a specific abduction mechanism, e.g. the one available in ABDUAL, both abducible and neg_abducible remain undefined in the Well-Founded Model (WFM), but may hold (as alternatives) in some Partial Stable Models.
Using the SM semantics abduction is done by guessing the truth-value of each abducible and providing the whole model and testing it for stability; whereas using the WFS with abduction, it can be performed by need, induced by the top-down query solving procedure, solely for the relevant abducibles — i.e., irrelevant abducibles are left unconsidered. Thus, top-down abductive query answering is a means of finding those abducible values one might commit to in order to satisfy a query.
An additional situation, addressed in this paper, is when one wishes to only passively determine which abducibles would be sufficient to satisfy some goal but without actually abducing them, just consuming other goals’ needed and produced abductions. The difference is subtle but of importance, and it requires a new construct. Its mechanism, of inspecting without abducing, can be conceived and implemented through metaabduction, and is discussed in detail in the sequel.
Backward and Forward Chaining Abductive query-answering is intrinsically a backward-chaining process, a top-down dependency-graph oriented proof-procedure. Finding the side-effects of a set of abductive assumptions may be conceptually envisaged as forward-chaining, as it consists of progressively deriving conclusions from the assumptions until the truth value of the chosen side-effect literals is determined.
The problem with full-fledged forward-chaining is that too many (often irrelevant) conclusions of a model are derived. Wasting time and resources deriving them only to be discarded afterwards is a flagrant setback. Worse, there may be many alternative models satisfying an abductive query (and the ICs) whose differences just repose on irrelevant conclusions. So unnecessary computation of irrelevant conclusions can be compounded by the need to discard irrelevant alternative complete models too.
A more intelligent solution would be afforded by selective forward-chaining, where the user would be allowed to specify those conclusions she is focused on, and only those would be computed in forward-chaining fashion. Combining backward-chaining with selective forward-chaining would allow for a greater precision in specifying what we wish to know, and improve efficiency altogether. In the sequel we show how such a selective forward chaining from a set of abductive hypotheses can be replaced by backward chaining from the focused on conclusions — the inspection points — by virtue of a controlled form of abduction which, never performing extra abductions, just checks for abducibles assumed elsewhere.
Meta-abduction is used in abduction inhibited inspection. Intuitively, when an abducible is considered under mere inspection, meta-abduction abduces only the intention to a posteriori check for its abduction elsewhere, i.e. it abduces the intention of verifying that the abducible is indeed adopted, but elsewhere. In practice, when we want to meta-abduce some abducible ‘x’, we abduce a literal ‘consume(x)’ (or ‘abduced(x)’), which represents the intention that ‘x’ is eventually abduced elsewhere in the process of finding an abductive solution. The check is performed after a complete abductive answer to the top query is found. Operationally, ‘x’ will already have been or will be later abduced as part of the ongoing solution to the top goal.
Example 9. Relevant and irrelevant side-effects. Consider this logic program where drink_water and drink_beer are abducibles.
thirsty; not drink: wet_glass use_glass: drink drink_water: thirsty: unsaf e_drive inspect(drunk): % This is an Integrity Constraint use_glass drink: drink drink_beer: drunk drink_beer:
Suppose we want to satisfy the Integrity Constraint, and also to check if we get drunk or not. However, we do not care about the glass becoming wet — that being completely irrelevant to our current concern. In this case, full forward-chaining or computation of whole models is a waste of time, because we are interested only in a subset of the program’s literals. What we need is a selective ersatz forward chaining mechanism, an inspection tool which permits to check the truth value of given literals as a consequence of the abductions made to satisfy a given query plus any Integrity Constraints.
Moreover, in this example, if we may simply want to know the side-effects of the possible actions in order to decide (to drive or not to drive) after we know which sideeffects are true. In such case, we do not want to the IC not unsaf e_drive because that would always impose not drink_beer. We want to allow all possible solutions for the single IC thirsty; not drink and then check the side-effects of each abductive solution.
Example 10. Police and Tear Gas Issue. Consider this other NLP, where ‘tear_gas’, ‘f ire’, and ‘water_cannon’ are the only abducibles. Notice that inspect is applied to calls.
police; riot; not contain: contain tear_gas: smoke f ire: police: % this is an Integrity Constraint contain water_cannon: smoke inspect(tear_gas): riot:
Notice the two rules for ‘smoke’. The first states that one explanation for smoke is fire, when assuming the hypothesis ‘f ire’. The second states ‘tear_gas’ is also a possible explanation for smoke. However, the presence of tear gas is a much more unlikely situation than the presence of fire; after all, tear gas is only used by police to contain riots and that is truly an exceptional situation. Fires are much more common and spontaneous than riots. For this reason, ‘f ire’ is a much more plausible explanation for ‘smoke’ and, therefore, in order to let the explanation for ‘smoke’ be ‘tear_gas’, there must be a plausible reason — imposed by some other likely phenomenon. This is represented by inspect(tear_gas) instead of simply ‘tear_gas’. The ‘inspect’ construct disallows regular abduction — only allowing meta-abduction — to be performed whilst trying to solve ‘tear_gas’. I.e., if we take tear gas as an abductive solution for smoke, this rule imposes that the step where we abduce ‘tear_gas’ is performed elsewhere, not under the derivation tree for ‘smoke’. Thus, ‘tear_gas’ is an inspection point. The IC, because there is ‘police’ and a ‘riot’, forces ‘contain’ to be true, and hence, ‘tear_gas’ or ‘water_cannon’ or both, must be abduced. ‘smoke’ is only explained if, at the end of the day, ‘tear_gas’ is abduced to enact containment. Abductive solutions should be plausible, and ‘smoke’ is plausibly explained by ‘tear_gas’ if there is a reason, a best explanation, that makes the presence of tear gas plausible; in this case the riot and the police. Plausibility is an important concept in science, for lending credibility to hypotheses. Assigning plausibility measures to situations is an orthogonal issue. In this example, another way of viewing the need for the new mechanism embodied by the inspect predicate is to consider we have 2 agents: one is a police officer and has the possibility of abducing (corresponding to actually throwing) tear_gas; the other agent is a civilian who, obviously, does not have the possibility of abducing (throwing) tear_gas. For the police officer agent, having the smoke inspect(tear_gas) rule, with the inspect is unnecessary: the agent knows that tear_gas is the explanation for smoke because it was himself who abduced (threw) tear_gas; but for the civilian agent the inspect in the smoke inspect(tear_gas) rule is absolutely indispensable, since he cannot abduce tear_gas and therefore cannot know, without inspecting, if that is the real explanation for smoke.
Example 11. Nuclear Power Plant Decision Problem. This example was extracted from [31] and adapted to our current designs, and its abducibles do not represent actions. In a nuclear power plant there is decision problem: cleaning staff will dust the power plant on cleaning days, but only if there is no alarm sounding. The alarm sounds when the temperature in the main reactor rises above a certain threshold, or if the alarm itself is faulty. When the alarm sounds everybody must evacuate the power plant immediately! Abducible literals are cleaning_day, temp_rise and f aulty_alarm. dust sound_alarm sound_alarm evacuate cleaning_day; inspect(not sound_alarm) temp_rise f aulty_alarm sound_alarm not cleaning_day
Satisfying the unique IC imposes cleaning_day true and gives us three minimal abductive solutions: S1 = fdust; cleaning_dayg, S2 = fcleaning_day; sound_alarm; temp_rise; evacuateg, and S3 = fcleaning_day; sound_alarm; f aulty_alarm; evacuateg. If we pose the query ? not dust we want to know what could justify the cleaners dusting not to occur given that it is a cleaning day (enforced by the IC). However, we do not want to abduce the rise in temperature of the reactor nor to abduce the alarm to be faulty in order to prove not dust. Any of these justifying two abductions must result as a side-effect of the need to explain something else, for instance the observation of the sounding of the alarm, expressible by adding the IC not sound_alarm, which would then abduce one or both of those two abducibles as plausible explanations. The inspect=1 in the body of the rule for dust prevents any abduction below sound_alarm to be made just to make not dust true. One other possibility would be for two observations, coded by ICs not temp_rise or not f aulty_alarm, to be present in order for not dust to be true as a side-effect. A similar argument can be made about evacuating: one thing is to explain why evacuation takes place, another altogether is to justify it as necessary side-effect of root explanations for the alarm to go off. These two pragmatic uses correspond to different queries: ? evacuate and ? inspect(evacuate), respectively. A simple transformation maps programs with inspection points into programs without them. Mark that the Stable Models of the transformed program where each abducible(X) is matched by the abducible X (X being a literal a or its default negation not a) clearly correspond to the intended procedural meanings ascribed to the inspection points of the original program.
Definition 11. Transforming Inspection Points. Let P be a program containing rules whose body possibly contains inspection points. The program (P ) consists of:
– inspect(not L) with not inspect(L); – inspect(a) or inspect(abduced(a)) with abduced(a) if a is an abducible, and keeping inspect(L) otherwise.
inspect(A) L01; : : : ; L0t where for every 1 i t: L0i = 8 abduced(Li) if Li is an abducible < inspect(X) if Li is inspect(X) : inspect(Li) otherwise
The semantics of the inspect predicate is given by the generated rules for inspect Example 12. Transforming a Program P with Nested Inspection Levels. x z a; inspect(y); b; c; not d d y y inspect(not a) b; inspect(not z); c Then, (P ) is: x inspect(x) y y inspect(y) inspect(y) z inspect(z) a; inspect(y); b; c; not d abduced(a); inspect(y); abduced(b); abduced(c); not abduced(d) not inspect(a) b; not inspect(z); c not abduced(a) abduced(b); not inspect(z); abduced(c) d abduced(d) The abductive stable model of (P ) respecting the inspection points is: fx; a; b; c; abduced(a); abduced(b); abduced(c); inspect(y)g.
Note that for each abduced(a) the corresponding a is in the model.
8.2 Inspection Points Implementation
Once again, we based our inspection point practical implementation on a formally
defined, XSB-implemented, true and tried abduction system — ABDUAL [
The query processing technique in ABDUAL relies on a mixture of program transformation and tabled evaluation. A transformation removes default negative literals (by making them positive) from both the program and the integrity rules. Specifically, a dual transformation is used, that defines for each objective literal O and its set of rules R, a dual set of rules whose conclusions not (O) are true if and only if O is false in R. Tabled evaluation of the resulting program turns out to be much simpler than for the original program, whenever abduction over negation is needed. At the same time, termination and complexity properties of tabled evaluation of extended programs are preserved by the transformation, when abduction is not needed. Regarding tabled evaluation, ABDUAL is in line with SLG [33] evaluation, which computes queries to normal programs according to the well-founded semantics. To it, ABDUAL tabled evaluation adds mechanisms to handle abduction and deal with the dual programs.
ABDUAL is composed of two modules: the preprocessor which transforms the
original program by adding its dual rules, plus specific abduction-enabling rules; and a
meta-interpreter allowing for top-down abductive query solving. When solving a query,
abducibles are dealt with by means of extra rules the preprocessor added to that
effect. These rules just add the name of the abducible to an ongoing list of current
abductions, unless the negation of the abducible was added before to the lists failing
in order to ensure abduction consistency. Meta-abduction is implemented adroitly by
means of a reserved predicate, ‘inspect=1’ taking some literal L as argument, which
engages the abduction mechanism to try and discharge any meta-abductions performed
under L by matching with the corresponding abducibles, adopted elsewhere outside
any ‘inspect=1’ call. The approach taken can easily be at least partially adopted by
other abductive systems, as we had the occasion to check with the authors [
Procedurally, in the ABDUAL implementation, the checking of an inspection point corresponds to performing a top-down query-proof for the inspected literal, but with the specific proviso of disabling new abductions during that proof. The proof for the inspected literal will succeed only if the abducibles needed for it were already adopted, or will be adopted, in the present ongoing solution search for the top query. Consequently, this check is performed after a solution for the query has been found. At inspectionpoint-top-down-proof-mode, whenever an abducible is encountered, instead of adopting it, we simply adopt the intention to a posteriori check if the abducible is part of the answer to the query (unless of course the negation of the abducible has already been adopted by then, allowing for immediate failure at that search node.) That is, one (meta - ) abduces the checking of some abducible A, and the check consists in confirming that A is part of the abductive solution by matching it with the object of the check. According to our method, the side-effects of interest are explicitly indicated by the user by wrapping the corresponding goals subject to inspection mode, with the reserved construct ‘inspect=1’.
We have recapped the LSMs semantics for all NLPs, complying with desirable requirements: 2-valued semantics, conservatively extending SMs, guarantee of model existence, relevance and cumulativity, plus respecting the WFM.
In the context of abductive logic programs, we presented a new mechanism of
inspecting literals that can check for side-effects of top-down driven 2-valued abductive
solutions, enabled by a form of meta-abduction, and have provided for it a declarative
semantics that relies on the relevance property of Layer Supported Model semantics.
We implemented this inspection mechanism within the Abdual [
We have also exhibited a space and time linearly complex transformation, TR, from one propositional NLP into another, whose Layer Supported Models are precisely the Stable Models of the transform, which can then be computed by extant Stable Model implementations. TR can be used to answer queries but is also of theoretical interest, for it may be used to prove properties of programs. Moreover, it can be employed in combination with the top-down query procedure of XSB-Prolog, and be applied solely to the residual program corresponding to a query. The XSB-XASP interface subsequently allows the program transform to be sent for Smodels for 2-valued evaluation. 9.1
Coda Prolog has been till recently the most accepted means to codify and execute logic programs, and a useful tool for research and application development in logic programming. Several stable implementations were developed and refined over the years, with plenty of working solutions to pragmatic issues, ranging from efficiency and portability to explorations of language extensions. XSB-Prolog is one of the most sophisticated, powerful, efficient and versatile, focusing on execution efficiency and interaction with external systems, implementing logic program evaluation following the Well-Founded Semantics (WFS).
The XASP interface [
Having defined a more general 2-valued semantics for NLPs much remains to be explored, in the way of properties, complexity, comparisons, implementations, extensions and applications, The applications afforded by LSMs are all those of SMs, plus those where odd loops over default negation (OLONs) are actually employed for problem domain representation, as we have shown in examples 7 and 8. The guarantee of model existence is essential in applications where knowledge sources are diverse (like in the Semantic Web), and wherever the bringing together of such knowledge (automated or not) can give rise to OLONs that would otherwise prevent the resulting program from having a semantics, thereby brusquely terminating the application. A similar situation can be brought about by self- and mutually-updating programs, including in the learning setting, where unforeseen OLONs would stop short an ongoing process if the SM semantics were in use.
That the LSM semantics includes the SM semantics and that it always exists and admits top-down querying is a novelty making us look anew at 2-valued semantics use in KRR. LSMs’ implementation, because of its relevance property, can avoid the need to compute whole models and all models, and hence SM’s apodictic need for complete groundness and the difficulties it begets for problem representation. Hence, apparently there is only to gain in exploring the adept move from SM semantics to the more general LSM one, given that the latter is readily implementable through the program transformation TR, introduced here for the first time.
Work under way concerns an XSB engine level efficient implementation of the LSM semantics, and the exploration of its wider scope of applications with respect to ASP, and namely in combination with abduction and constructive negation.
One topic of future work consists in defining partial model schemas, that can provide answers to queries in terms of abstract non-ground model schemas encompassing several instances of ground partial models. Abstract partial models, instead of ground ones, may be produced directly by the residual, a subject for further investigation.
Yet another topic of future exploration is the definition of a Well-Founded Layer Supported Model (WFLSM). Conceivably, the WFLSM would be defined as a partial model that, at each layer, is the intersection of the all LSMs. Floating conclusions are consequently disallowed. Incidental to this topic is the relationship of the WFLSM to O-semantics [26], it being readily apparent the former extends the latter.
Finally, the concepts and techniques introduced in this paper are might be adoptable by other logic programming systems and implementations. 10
We thank Marco Alberti, José Júlio Alferes, Pierangelo Dell’Acqua, Robert Kowalski, Juan Carlos Nieves, Mauricio Osorio, and David Warren for their comments. 14. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In
ICLP/SLP, pages 1070–1080. MIT Press, 1988. 15. M. Gelfond, H. Przymusinska, V. Lifschitz, and M. Truszczynski. Disjunctive defaults. In
KR-91, pages 230–237, 1991. 16. P. Hitzler and M. Wendt. A uniform approach to logic programming semantics. TPLP, 5(1-2):93–121, 2005. 17. K. Inoue and C. Sakama. A fixpoint characterization of abductive logic programs. Journal of Logic Programming, 27(2):107–136, 1996. 18. A. Kakas, R. Kowalski, and F. Toni. The role of abduction in logic programming. In Handbook of Logic in AI and LP, volume 5, pages 235–324. Oxford University Press, 1998. 19. I. Niemelä and P. Simons. Smodels - an implementation of the stable model and well-founded semantics for normal logic programs. In Procs. LPNMR’97, LNAI, vol. 1265, pp. 420–429, 1997. 20. J. C. Nieves, M. Osorio, and C. Zepeda. Expressing extension-based semantics based on stratified minimal models. In Logic, Language, Information and Computation, volume 5514 of LNCS, pages 305–319. Springer, 2009. 21. L. M. Pereira and A. M. Pinto. Revised stable models - a semantics for logic programs. In
G. Dias et al., editor, Progress in AI, volume 3808 of LNCS, pages 29–42. Springer, 2005. 22. L. M. Pereira and A. M. Pinto. Approved models for normal logic programs. In N. Dershowitz and A. Voronkov, editors, Procs. LPAR’07, LPAR - LNAI, Yerevan, Armenia, October 2007. Springer. 23. L. M. Pereira and A. M. Pinto. Inspection points and meta-abduction in logic programs. In
INAP’09, LNCS. Springer, 2009. 24. L. M. Pereira and A. M. Pinto. Layer supported models of logic programs. In Procs. 10th LPNMR, LNCS, pages 450–456. Springer, September 2009. Long version at http://centria.di.fct.unl.pt/ lmp/publications/online-papers/LSMs.pdf. 25. L. M. Pereira and A. M. Pinto. Stable model implementation of layer supported models by program transformation. In INAP’09, LNCS. Springer, 2009. 26. L.M. Pereira, J.J. Alferes, and J.N. Aparício. Adding closed world assumptions to wellfounded semantics. TCS, 122(1-2):49–68, 1994. 27. L.M. Pereira and A.M. Pinto. Layered models top-down querying of normal logic programs.
In Procs. PADL’09, volume 5418 of LNCS, pages 254–268. Springer, January 2009. 28. T. C. Przymusinski. Every logic program has a natural stratification and an iterated least fixed point model. In PODS, pages 11–21. ACM Press, 1989. 29. T. C. Przymusinski. Well-founded and stationary models of logic programs. Annals of
Mathematics and Artificial Intelligence, 12:141–187, 1994. 30. T.C. Przymusinski. Perfect model semantics. In ICLP/SLP, pages 1081–1096, 1988. 31. F. Sadri and F. Toni. Abduction with negation as failure for active and reactive rules. In
AI*IA, pages 49–60, 1999. 32. T. Swift. Tabling for non-monotonic programming. Annals of Mathematics and Artificial
Intelligence, 25(3-4):201–240, 1999. 33. T. Swift and D. S. Warren. An abstract machine for slg resolution: Definite programs. In
Symp. on Logic Programming, pages 633–652, 1994. 34. R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Computing, 1(2):146–160, 1972.