From: Axel Polleres <axel.polleres@deri.org>

Date: Fri, 06 Jul 2007 01:19:32 +0100

Message-ID: <468D8A94.9060003@deri.org>

To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Date: Fri, 06 Jul 2007 01:19:32 +0100

Message-ID: <468D8A94.9060003@deri.org>

To: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

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.... axelReceived on Friday, 6 July 2007 00:19:55 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:46 UTC
*