[Arch] Action 319

This mail addresses Action Item
http://www.w3.org/2005/rules/wg/track/actions/319
"Develop strawman for stratified NAF extension, then extend it to 
well-founded and stable negation (three related extensions)."


Since, I am not clear on how to define an extension of core, I guess, it 
was the goal to of this exercise to raise issues on just starting and 
trying...
  I am not at all sure whether what I do here is how this exercise was 
intended to be conducted, but let's give it a "strawman"-try anyway:


Prelude:
-------

The dialects/extension we want to model here are non-ground
(Stratified) Normal Logic Programs under the well-founded or stable 
model semantics.
Dialect1: Stratified Normal Logic Programs
Dialect2: Normal Logic Programs under the well-founded Semantics
Dialect3: Normal Logic Programs under the stable model Semantics


Normal Logic Programs are Horn rules extended with allowing
atoms negated with negation as failure (naf)  in rule bodies.

i.e. rules of the form:

   h impliedBy b_1 and b_2 and ... and b_n

where h is ATOMICs and b_1 ... b_n either atoms or naf-negated ATOMICs
(usually only uniterms considered and not necessarily equality in heads,
variables implicitly all-quantified over the whole rule)

"Stratified" means that these rules have the following restriction the 
on the use of naf over rulesets:

   No predicate appearing in a rule head recursively depends on it self 
via a negated body literal.

For normal logic programs, there exist two deviating standard semantics,
the well-founded semantics [1] and the stable model semantics [2],
which, as widely known coincide on stratified programs. Since these
two semantics  deviate on their treatment of negation as failure, we
will in the following also speak about well-founded negation as failure
(wfnaf) and stable-model negation as failure (smnaf)



Syntax:
-------

I will first discuss how the RIF core syntax needs to be extended to 
cater for Dialect1 - Dialect3. When taking RIF Core as the basis and 
compare with thw standard definition for normal logic programs above, we 
strictly
speaking allow more than normal logic program since we allow
  (i) disjunction in rule bodies as well as
  (ii) equality in rule heads which
  (iii) frames and sorts

ad (i) should not be a problem
ad (ii) I need to check how whether/how equality in heads is
         considered in stratified programs or whether it is problematic,
         I for the moment optimistically assume no, if anybody has a
         pointer, I'd be grateful, but I have no possiblity to check now.
ad (iii) frames are syntactic sugar only, so I'd assume they carry over
         without problems as well, as for sorted constants, I also see
         no problems upfront


We need the following syntactic extensions to model the three dialects
compared to RIF Core Rules

  + three kinds default negated atoms I will extend our current asn06
    model for this, marking additions with '+'

-----------------------------------------------------
class CONDITION

     subclass And
         property formula : list of CONDITION

     subclass Or
         property formula : list of CONDITION

     subclass Exists
         property declare : list of Var
         property formula : CONDITION

     subclass ATOMIC

+   subclass naf
+       property ATOM : ATOMIC
+       subclass wfnaf
+       subclass smnaf
-----------------------------------------------------
  It seems, for the simple extension of normal logic programs,
these forur lines are good enough. There are extensions of logic 
programs which add more syntactivally, like allowing disjunctive heads,
allowing negation as failure in the head, etc.

Now while this syntactic extension is say general for normal logic 
programs it is not so clear how we could disambiguate the 3 subdialects
Dialect1-Dialect3 here. For all these, it seems we need syntactic 
restrictions not expressible in asn06.

Dialect1: For Dialect1 we need a syntactic condition over the
    ruleset for being stratified. Sine this is not a condition which
    we can "express" in asn06, I could use the LP-style constraint
    approach, proposed during the one but last f2f, see:
http://lists.w3.org/Archives/Public/public-rif-wg/2007Feb/att-0083/RIFRAFOntology.pdf

   unstratified neagtion in a ruleset could be checked something like:
   --------------------------------------------------------------
   HASUNSTRATIFIEDNEGATION :- negDep(P1,P1,RS).


   recHasCondition(X,C1) :- hasCondition(X,C).
   recHasCondition(X,C1) :- hasCondition(X,C0), hasCondition(C,C1).

   dep(P1,P2,RS) :- ruleset(RS),hasRule(RS,R),hasHead(R,H),hasBody(R,B)
                    Uniterm(H), hasOp(H,P1), recHasCondition(B,C)
                    Uniterm(C), hasOp(C,P2).
   dep(P1,P3,RS) :- dep(P1,P2,RS), dep(P2,P3,RS).

negdep(P1,P2,RS) :- ruleset(RS),hasRule(RS,R),hasHead(R,H),hasBody(R,B)
                    Uniterm(H), hasOp(H,P1), recHasCondition(B,C)
                    naf(C), hasAtom(C,A), Uniterm(A) hasOp(A,P2).

  negdep(P1,P2,RS) :- negdep(P1,P2,RS), dep(P2,P3,RS).
  negdep(P1,P2,RS) :- dep(P1,P2,RS), negdep(P2,P3,RS).
  negdep(P1,P2,RS) :- negdep(P1,P2,RS), negdep(P2,P3,RS).
   --------------------------------------------------------------


Dialect2: For Dialect2, I need to restrict all uses of naf to wfnaf.

Dialect3: For Dialect3, I need to restrict all uses of naf to smnaf.


I could think of RIF Core as Dialect0 here, whereI need to restrict
CONDITIONS not to contain any naf.

I could think of a super-dialect 4 which though has an unclear semantics
mixing well-founded and stable semantics. Results on the logical 
formalisation of both, stable and well-founded negation under one 
framework [3,4,5,6,7] could serve as a basis, but I would still consider 
this a topic of research and not (yet) a RIF issue, since also these 
works cover mostly the propositional case only.


Issues/questions:
-----------------

- May I subclass classes and reuse their properties as I do here for
naf,wsnaf,smnaf?

- If I add some subclasses to CONDITION, as proposed here for extending 
Core, would I not change the menaing of CONDITION and thus RULESET, anf 
thus Core? Or would I need to redefine CONDITION/RULESET by new classes 
in such an extension?

Issue1: We need to clarify what an extension of a dialect may add
  and how.

Issue2: We need to clarify how to model/state syntactic or other dialect 
restrictions whioch cannot be expressed in asn06.


Compatibility/Semantics:
------------------------

*  FWD Compatibility:  "A RIF dialect is forward compatible if a 
conformant implementation will process instances of any future or 
unknown extension according to the specification of the said
    extension."

  I'd guess Core is unlikely to be Forward compatible towards
  Stratified Normal Logic Programs as described here,
  however, by ignoring
    (i)  all naf atoms with predicate symbols not occurring in any
         rule head in the rule set
    (ii) deleting all rules involving naf, after
         applying (i)
  one could achieve a soundness-preserving treatment.

* Backward compatibility: Dialects 2 and 3 should both be backwards 
compatible with Dialect 1. However, I am not sure about whether/what we 
mean by backwards compatiblity with Core. I'd guess, e.g. the logics 
presented in [6] could serve as a backwards compatible extension of
Horn towards Dialect1 and Dialect3.


References:


1. A. Van Gelder, K. Ross, and J.S. Schlipf. Unfounded sets and well- 
founded semantics for general logic programs. In 7th ACM Symposium on 
Principles of Database Systems, Austin, Texas, 1988.
2. M. Gelfond and V. Lifschitz. The stable model semantics for logic 
programming. In 5th Int’l Conf. on Logic Programming, Cambridge, 
Massachusetts, 1988.
3. Piero A. Bonatti. Autoepistemic logics as a unifying
framework for the semantics of logic programs. Journal
of Logic Programming, 22(2):91–149, 1995.
4. Teodor C. Przymusinski. Autoepistemic logic of knowl-
edge and beliefs. Artificial Intelligence, 95:115–154,
1997.
5. Marc Denecker, V. Wiktor Marek, and Miroslaw
Truszczynski. Uniform semantic treatment of default and autoepistemic 
logics. Artificial Intelligence,
143(1):79–122, 2003.
6. David Pearce and Agustín Valverde.
Quantified Equilibrium Logic and the First Order Logic of 
Here-and-There. Technical Report, Univ. Rey Juan Carlos, 2006
7. Pedro Cabalar, Sergei Odintsov, David Pearce and Agustín Valverde.
Analysing and Extending Well-Founded and Partial Stable Semantics using 
Partial Equilibrium Logic, Proceedings of ICLP 2006, Springer LNCS 4079, 
2006, 346-360.



hope this was somehow what was expected....

axel

Received on Friday, 6 July 2007 00:19:55 UTC