daml rules document strawman v1

From: Benjamin Grosof ([email protected])
Date: 07/08/03

  • Next message: Benjamin Grosof: "notes from today's JC telecon on DAML Rules strawman and plans"
    % v1 "strawman" draft of DAML-Rules
    DAML Rules Strawman for the Joint Committee
    by Benjamin Grosof
    Draft of July 8, 2003
    This is an initial, quite partial, quite early, version, i.e., a "strawman"
    to help kick work off.  It responds to an action item from the 6/24/2003
    JC telecon.
    "DAML Rules" is a strawman name for the rule language product of
    the Joint Committee.  A key input for DAML Rules is RuleML.
    This first version addresses:
    - syntax
    - semantics
    - an initial list of issues
    Mainly, it is to "staple together" some relevant documents already
    previously posted and discussed.
    The ideas in this reflect the contributions of a number of other
    people on the Joint Committee and in RuleML Initiative.  Proper
    credits should/will come soon in a revised version.
    SECTION 1:   Motivations:  Requirements and Objectives
    (to be written)
    SECTION 2:  Semantics
    Our initial consensus about the expressiveness and semantics of the
    rules language appears to be:
    1. at least: the expressiveness of Horn Logic Programs, as in RuleML.
    2. plus then some extensions:  some perhaps in V1 of the rule language,
    others in later versions V2+.
    Some of these extensions include:
    - Explicit Equality
    - Horn FOL expressiveness
    - Lloyd-Topor LP reducible to Horn LP, e.g., permit AND in head, OR in body.
    - Negation As Failure
    - Prioritization
    - Procedural Attachments and built-ins
    These extensions are mentioned more in section 4 (Issues and Roadmap).
    A substantial expressive subset of OWL can be translated into Horn LP,
    using the approach of Description Logic Programs (DLP).
    Grosof, B., Horrock, I., Volz, R., Decker. S., "Description Logic Programs:
    Combining Logic Programs with Description Logic", Proc. WWW- 2003.
    SUBSECTION 2.1:  Semantics of Horn Logic Programs
    % Draft of a self-contained writeup on the standard
    % (least fixed point / least Herbrand model) semantics of Horn logic programs.
    % That semantics is normative for the Horn logic programs sublanguage of 
    % The corresponding current RuleML DTD is
    % http://www.ruleml.org/dtd/0.8/ruleml-urhornlog-monolith.dtd ;
    % that also includes some extra syntactic features (e.g., URI constant names,
    % unordered argument collections)
        Horn Logic Program Semantics for RuleML
        Benjamin Grosof
        MIT Sloan School of Management
        [email protected]   http://ebusiness.m   http://ebusiness.mit.edu/bgrosof
        Draft of May 9, 2003
    The language of a Horn logic program, like a first-order language
    signature, is determined by its individual constants,
    (logical-)function constants, and predicate constants -- these
    together are called its *signature*.  A (logical-)function is also
    known as a constructor.  An individual constant is sometimes also
    known as an object constant.  A function has arity greater than 0.
    (Note that this is easy to generalize; one can view an individual
    constant as a function constant with arity zero.)  Terms are built as
    in the corresponding first-order language.  Atoms have the form
    p(t_1,...,t_n), where the t's are terms and p is a predicate symbol of
    arity n.  "LP" abbreviates "logic program".
    A Horn rule (a.k.a. definite rule) is an expression of the form
       H <- B_1 /\ ... /\ B_m .                         (1)
    where B_i's are atoms, m is greater-than-or-equal to zero (i.e., m >=
    0), and "/\" stands for logical conjunction.  ("/\" is sometimes
    written as "and".)  The left-hand side of the rule is called the
    rule's head or consequent; the right-hand is called the rule's body or
    antecedent.  "<-" is called implication, and intuitively can be read
    as "if".  (Note that "<-" is similar to, but not quite the same as,
    material implication in classical logic.)  A collection of Horn rules
    is called a Horn logic program.  It is also referred to as a definite
    logic program.  A logic program is also called a rulebase.  Formulas
    and rules not containing variables are called ground.  Unless
    otherwise stated, the notational convention is that logical variable
    are prefixed with a "?".  If m=0 and H is ground, then the rule is
    called a *fact*.  More generally, if m=0, the "<-" may be omitted
    notationally.  In this case, the body is empty and is defined to be
    equivalent logically to True.  E.g., a fact H (where H is ground) can
    be written simply as:
       H .
    In Prologs, the usual notational convention is that variables begin with a
    capital letter, "<-" is replaced by ":-", and "/\" is replaced by ",".
    For a FOL formula E[?x1,...,?xm] whose free variables are ?X=(?x1,...,?xm),
    we say that (for all ?X. E[?X]) (respectively, (there exists ?X. E[?X]))
    is the *universal closure* (respectively, *existential closure*) of E.
    Another way we speak of this is to say that E is universally
    (respectively, existentially) quantified at outermost scope.
    Notationally, in writing a universal or existential closure, sometimes
    we simply omit the variables immediately after the quantifier.
    We define the *classical version* of the rule (1)
    to be the Horn FOL axiom to be the universal closure of rule (1),
    where "<-" is treated as material implication.
    Likewise, we define the classical version of a Horn LP rulebase R to
    consist of the classical versions of every rule in R.
    In Horn *LP*, each rule of form (1) can be viewed as universally
    quantified at outermost scope, with the notation simply leaving this
    quantification implicit.  However, note that the usual definition of
    the semantics of Horn LP (i.e., the one we give below, called the
    least fixed point semantics) does not use the formal notion of a
    universal quantifier *within* the language.
    The set of all ground terms in the language of a rulebase R will be
    denoted by HU(R) (Herbrand universe of R) with R omitted notationally
    whenever possible.  The set of all ground atoms in the language of a
    rulebase R will be denoted by HB(R) (Herbrand base of R) with R
    omitted notationally whenever possible.  For a predicate p, atoms (p)
    will denote the subset of HB(R) formed with predicate p.  For a set of
    predicates Q, atoms(Q) will denote the subset of HB(R) formed with the
    predicates in Q.
    Unless stated otherwise, a rule with variables stands for the set of
    all its ground instantiations; and thus, likewise, a rulebase (where
    some rules contain variables) stands for the set of all its ground
    instantiations.  Note that a rule without variables trivially stands
    for the set of all its ground instantiations.  Note also that the
    ground instantiations of a rulebase consist of all the ground
    instantiations of all of its rules.  Thus we can restate the previous
    three sentences more simply as: a rulebase stands for the set of all
    its ground instantiations.
    The form of a *normal* logic program, a.k.a. "ordinary" logic program
    (also sometimes known as a "general" [sic] logic program -- but
    there are actually several further generalizations), generalizes
    that of a Horn logic program, so as to permit body literals to
    be negated by negation-as-failure.  A rule in a normal logic program
    is an expression of the form:
       H <- B_1 /\ ... /\ B_m /\ ~B_m+1 /\ ... /\ ~B_n .           (2)
    where "~"stands for negation-as-failure (NAF).
    The *model* of a Horn logic program R is the smallest subset S of HB
    such that for any rule of form (1) in R, if B_1, ..., B_m are each
    in S, then H is also in S.  Notationally, this model is denoted by mod(R).
    A way to view this definition is that the model of R is the least fixed
    point of a certain operator T_R, which we define below.
    This definition is thus also known as the "least fixed point" semantics.
    The model of R is also known as the "least Herbrand model" or
    "least fixed point model".
    Definition of Operator T_R:
    Let R_1 be a ground rule of form (1).
    We define an operator T_R1 which takes as input any subset V of HB,
    and which generates as output a subset W of HB, where W is a superset of V.
    The operator T_R1 adds the head of R1 to W if the body of R1 is satisfied
    in V; if not,  W is just the same as V.
        T_R1 : 2^HB -> 2^HB
        if  B_1, ..., B_m are each in V, then W = (V union {H}),
        else W=V.
    Intuitively, the operator T_R1 represents the effect of a
    single iteration of applying the rule R_1 to a working fact set V
    (e.g., intermediate conclusions in the course of inferencing).
    If the rule's body is satisfied, i.e., if the rule fires,
    then the rule's head is added to the new working fact set W.
    More generally, we extend this operator concept to sets of rules.
    Let R be a Horn logic program, consisting of rules R_1, ..., R_k.
    We define an operator T_R which takes as input any subset V of HB,
    and which generates as output a subset X of HB, where X is a superset of V.
    X = T_R(V) = the union of T_R1(V), ..., T_Rk(V).
    Intuitively, the operator T_R represents the effect of a
    single iteration of applying all the rules R_1,...,R_k to a working fact set V
    (e.g., intermediate conclusions in the course of inferencing).
    For each rule, if the rule's body is satisfied, i.e., if the rule fires,
    then the rule's head is added to the new working fact set X.
    Another way to view this intuitively is that T_R is the
    "constructive implication operator" for R.
    In the least fixed point semantics for Horn logic programs,
    the model of R is defined to be the least fixed point of T_R,
    i.e., the smallest subset S of HB such that S = T_R(S).
    (End of definition of T_R.)
    There are several different semantics for normal logic programs that
    have been defined in the literature; we recommend the well-founded
    semantics [Van Gelder et al 1991].
    For the case of definite logic programs, most (if not all) of these
    different semantics, including in particular the well-founded
    semantics, coincide with (i.e., are equivalent to) the
    least-fixed-point semantics.  More generally, most (if not all) of
    these different semantics coincide with the well-founded semantics,
    for the case of stratified logic programs.
    The various semantics for normal logic programs defined in the literature
    differ primarily in their treatment of certain non-stratified cases involving
    the interaction of negation-as-failure with cyclic dependencies
    among predicates or atoms.
    In this short paper, however, we will not be defining or discussing
    the detailed semantics of normal logic programs that do contain NAF.
    A ground atom A is *True* in S iff A is in S (i.e., if A is a member of S).
    Thus A is True in mod(R) iff A is in mod(R).  Iff A is True in mod(R),
    then A is said to be *entailed* by R, i.e., a *conclusion* of R,
    and to have *truth value* True.
    If A is not True in mod(R), then A is said to be not entailed by R, i.e.,
    not a conclusion of R.
    If A is not True in mod(R), A is also sometimes said to have truth
    value *Fail* or *NAF*.  Fail also often known as "*False*".  Note that
    in this context "False", however, does *not* correspond to classical falsity,
    i.e., to classical negation!  Rather it corresponds to negation-as-failure.
    Intuitively: if A has truth value Fail, then A is not believed;
    whereas, in *classical* logic, if A has truth value (classical-)false,
    then A is believed to be false, i.e., not-A is believed to be true.
    In *normal* logic programs, iff A has truth value *Fail*, then ~A is
    said to be True in mod(R).  Intuitively, *Fail* corresponds roughly to
    "either classically false or unknown".  The general semantics of NAF in normal
    LP's has subtleties, however. E.g., the well-founded semantics in
    general may assign a third truth value "*undefined*" to some atoms.
    The definition of entailment is extended to conjunctive
    formulas via the following truth recursion.
    A conjunction of ground atoms A_1 /\ ... /\ A_m is True
    iff each conjunct A_i (for i=1,...,k) is True.
    More generally, a conjunction is true iff one of its conjuncts is true.
    We call the above definition of entailment:  "*basic*" entailment.
    Query-answering in which bindings are returned is then straightforwardly
    defined.  Let the query formula be the existential closure of a
    conjunction of atoms.  Then entailed bindings correspond to the entailed
    ground instances of that conjunction of atoms.
    Relationship to Horn FOL:
    The model of R is the least Herbrand model, in the sense that
    it is the greatest lower bound w.r.t. inclusion.  That is,
    the model of R is exactly the set of ground atoms that are entailed
    in classical FOL semantics by the classical version of the Horn LP.
    Terminologically, "Horn clause" in FOL also permits the clause to
    havfe an empty head, i.e., for the clause to have no positive literal.
    A "Horn LP rule" as defined here does *not* permit the head to be
    empty.  In the LP literature an empty-head clause is often known as a
    "goal", or sometimes as an "integrity constraint" [sic].
    Classically Sound but Incomplete:
    Basic entailment is conservative in that it is "*classically sound*",
    by which we mean sound w.r.t. the classical (FOL) entailments of the
    classical version of the rulebase R (i.e., viewing R as a set of Horn
    FOL axioms).  In general, it is weaker than (i.e., incomplete w.r.t.)
    the classical entailment of the classical version of the rulebase R.
    Example:  Friendliness.
    For example, consider the following Horn LP rulebase G:
       friendly(?x) <- good(?x) .
       attractive(?x) <- friendly(?x) /\ bouncy(?x).
    This entails exactly the conclusions
       {good(fred), friendly(sue), bouncy(fred), friendly(fred), attractive(fred)}
    The classical version of G also entails various formulas which the
    Horn LP G does not; some of these are:
       friendly(sue) \/ friendly(fred).
       forall ?x.  attractive(?x) <- good(?x).
       attractive(sue) <- bouncy(sue).
       bouncy(fred) <- bouncy(fred).
       forall ?x. friendly(?x)  \/ bouncy(?x) <- friendly(?x).
       bouncy(sue) <-> attractive(sue).
       attractive(sue) \/ not attractive(sue).
    where "not" is classical negation and "<->" is classical equivalence.
    We call this list of non-entailed formulas "more-G-stuff", for
    later reference.
    Extensions of the definition of entailment:
    There is also a sizable LP KR literature that addresses *extensions* to
    this basic concept of entailment so as to answer queries in more
    general form.  These extensions can usually be viewed as reducing
    inferencing w.r.t. the extended entailment concept to inferencing w.r.t.
    the basic entailment concept.  For example, most or all
    of the formulas in more-G-stuff could be inferred by systems that
    use extended concepts of entailment.  However, we do not have
    space or focus to address these entailments in detail in this paper.
    Parts of this were adapted from [Baral and Gelfond 1994] and [Lloyd 1987].
    [Lloyd 1987] gives a good treatment of the semantic foundations of Horn LP
    (which is called "definite LP" there).
    [Baral and Gelfond 1994]
    Chitta Baral and Michael Gelfond, "Logic Programming and Knowledge
    Representation", J. Logic Programming, 1994.
    [Lloyd 1987]
    John W. Lloyd, Foundations of Logic Programming, Second, Extended
    edition, Springer, Berlin, 1987.
    [Van Gelder et al 1991]
    Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf,
    "The Well-Founded Semantics for General Logic Programs," J. ACM, 38:3,
    pp. 620-650, July 1991.  http://www.cs.columbia.edu/~kar/pubsk/wfjacm.ps.
    SUB SECTION 2.2:  Explicit Equality
    Draft of explicit axiomatization of equality for RuleML / DAML Rules
    by Benjamin Grosof
    version V1 of 7/1/03
    % (file housekeeping memo to Benjamin:  this file is axiomatization-1.txt,
    %  excerpted from file equality/thoughts-1.txt)
    Background:  see Joint Committee telecon discussion of 7/1/03, including
    - Mike Dean's test cases
    - Benj's notes from the telecon
    Here's a pass at defining an axiomatization, within a declarative
    (definite Horn) LP language itself,
    of explicit equality.  Here, equality is
    treated as essentially an ordinary predicate (rather than specially
    within the model theory).
    Let ee stand for the explicit equality predicate.
    1. symmetry:
       ee(?y,?x) <- ee(?x,?y);
    2. transitivity:
       ee(?x,?z) <- ee(?x,?y) and ee(?y,?z);
    3. substitutivity for predicates:
    Let P1,...,Pm be the predicates of the LP language.
    Let the arity of Pi be ni, where ni >= 0.
    For each Pi, i=1,...,m, and for each j=1,...,ni:
       Pi(?X1,...,?W,...,?Xni) <- ee(?Xj,?W) and Pi(?X1,...,?Xj,...,?Xni);
    Actually, one can equivalently omit this if ni=0.
    4. substitutivity for logical functions, i.e., constructors:
    Let F1,...,Fk be the logical functions of the LP language.
    Let the arity of Fi be ni, where ni >= 0.
    For each Fi, i=1,...,k, and for each j=1,...,ni:
              <- ee(?Xj,?W) and ee(?Y,Fi(?X1,...,?Xj,...,?Xni));
    Actually, one can equivalently omit this if ni=0.
    Issue/Q todo:  do we need to say anything else about equality other
    than the above (1.)-(4.)?
    - E.g., is there anything different about skolem functions?
    - E.g., is there something that needs to be said about how unification
    treats equality in corresponding proof theory (since the usual
    definition of unification ignores equality other than syntactic
    todo: Look at how FOL with equality has been formalized, including
    unification in it.
    SECTION 3:  Syntax
    Syntax needs to address both the needs of automated exchange and of
    human editing, e.g., discussion by human system designers or knowledge
    SUBSECTION 3.1:   Exchange Syntax
    An initial point of departure for exchange syntax is RuleML's current
    XML syntax, which is given below.  However, it would be helpful to
    integrate more easily with OWL syntax.
    Below is the current RuleML V0.8 syntax, described in abstract syntax
    using the GNBF notation which is a simple extension of EBNF.
    GBNF definition is given in an Appendix.
    % by Benjamin Grosof
    % created 3/28/03
    GBNF specification of:
            Hornlog (i.e., Horn Logic Programs),
            with the URI constants feature ("ur"), and
            with the object-oriented arguments collection feature ("roli's"),
            and with the experimental feature of a query statement ("query")
            element that was defined in some other versions of RuleML V0.8 Hornlog
    This version corresponds to the monolith V0.8 DTD for Hornlog with ur
    and roli's.
    /* in future, may delete the _rbschema part */
    rulebase : _rbaselab? , _statements , @direction , _rbschema ;
    _rbschema = @xmlns:xsi? , @xsi:noNamespaceSchemaLocation? ;
    /* @xmlns:xsi and @xsi:noNamespaceSchemaLocation optionally specify an
           XML Schema on the root element rulebase */
    @xmlns:xsi : URI ;
    @xsi:noNamespaceSchemaLocation : URI ;
    @direction : inferencingdirection ;
    inferencingdirection = FORWARD | BACKWARD | BIDIRECTIONAL ;
    @direction $ BIDIRECTIONAL ;
    _rbaselab : ind | cterm ;
    _statements = (imp | fact | query)*  ;
    imp : _rlab? , _head , _body  ;
    fact : _rlab? , _head ;
    query : _rlab? , _body ;
    _rlab : ind | cterm ;
    _head : classicalliteral ;
    _body : literal | complexbodyexpr ;
    literal = classicalliteral ;
    classicalliteral = atom ;
    complexbodyexpr = andbodyexpr ;
    andbodyexpr = and ;
    and : (atom)* ;
              /* recommend in revised design to replace and by andb,
                     where here have  andh : (literal)* ;
                     this would improve up-compatibility elegance */
    atom : _opr , _args ;
    _opr : rel ;
    _args = (logicalterm | argumentcollection)\* ;
              /* implicitly top-level is an ordered tuple */
    logicalterm = ind | var | cterm ;
    argumentcollection = tup | roli ;
    rel : constname ;
    constname = PCDATA , @href? ;
    @href : URI
    URI = CDATA ;
    var : PCDATA ;
    ind : constname ;
    cterm : _opc, _args ;
    _opc : ctor ;
    ctor : constname ;
    tup : (logicalterm | argumentcollection)\* ;
               /* implicitly at top-level is an ordered tuple.
                  permits nested tup's and roli's, in spirit of complex
                  data structures / Object-Oriented / Lisp S-expressions.  */
    roli : (_arv)* ;
    _arv  : arole, (logicalterm | argumentcollection) ;
    arole : constname ;
    /* Explanation of Abbreviations:
       rulebase = knowledge base of rules.
       direction = intended direction of inferencing.
       _rbaselab = rulebase label.  Name of a rulebase.
       imp = implication rule.
               (Note it does not employ *material* implication cf. classical 
       fact:  Can be viewed logically as an implication rule that has an empty 
       _head = head of a rule.  A.k.a. the "consequent" or "then" part of the rule.
       _body = body of a rule.  A.k.a. the "antecedent" or "if" part of the rule.
       _rlab = rule label.  Name of a rule.
       and = conjunctive body expression.  The "and" of some body atoms.
       atom = logical atom.  An expression formed from a predicate applied to a
                 collection of its (logical) arguments.
       _opr = relational operator expression.  (This is for sake of upward
                expressive extensibility.)
       rel = relation.  A logical predicate.
       var = variable.  A logical variable.
       ind = individual.  A logical individual.
                (Can be viewed logically as logical function whose arity is zero.)
       cterm = complex term.  A logical term of the form "f(...)" where f is a 
       _opc = constructor operator expression.  (Similar in spirit to _opr.)
       ctor = constructor.  A logical function.
       tup = tuple of arguments.  An ordered collection of arguments.
       roli = role'd list of arguments.  An unordered collection of arguments,
                with each member of the collecion being distinguished by an
                argument role name (arole).
       _arv = argument role-value pair.  An argument (value) together with its
                indicating argument role (arole).
       arole = argument role.  (See roli and _arv above.)
       query = stored query specification.  An EXPERIMENTAL feature.
       Note that in this DTD version, tup's and roli's can be nested.  This is an
         EXPERIMENTAL aspect of the object-oriented argument collections feature.
    SUBSECTION 3.2:   Human-oriented Syntax
    There have been a number of proposals on human-oriented syntax.
    It appears desirable to draw upon the best of Prolog (e.g., XSB),
    Jess (e.g., unordered slotnames for arguments, not just ordered "positions"),
    N3 (e.g., RDF), and CommonLogic (e.g., lists)
    SECTION 4:  Issues and Roadmap
    (more to be written beyond the following)
    SUBSECTION 4.1:  Integration with OWL
    SUBSECTION 4.2:  Roadmap
    todo:  To be added:  Michael Dean's suggestions document, updated.
    % suggestions wrt roadmap for Rules in the Joint Committee
    % by Benjamin Grosof
    % created 5/6/03
    % this version 5/27/03
    Currently, we have two loosely-coupled efforts:
    1. on Rules syntax and expressiveness, starting from RuleML
         and (to a lesser degree so far) Common Logic as primary points of 
    2. on use cases
    Both involve analysis of requirements.
    My suggestions for today address primarily (1.).
    (2.) should definitely continue and be coordinated increasingly
    closely with (1.).
    I suggest several phases, to tackle various issues; see below.
    I've probably forgotten to include some issues, and quite possibly
    some more will arise during our design efforts.  But I think
    I've listed at least most of the issues.
    Phase I:  we start with defining:
    o Datalog Horn logic programs, with URIrefs for predicate etc. logical
    constants, cf. RuleML; and
    coordinate/cross-fertilize this with the specification of
    Datalog Horn FOL in Common Logic.
    (Datalog here means without logical functions of non-zero arity.)
    o then Horn without the Datalog restriction
    Then extend with various additional features cf. RuleML's existing (V0.8)
    or currently-in-discussion designs, again coordinating this with
    the specification of Common Logic.
    Phase II: (taken as subset of what's listed in Phase III below)
    o built-ins:  relatively simple informational only
    . at least via some standard namespaces and user conventions
    -- i.e., as part of the rule inferencing environment
    . i.e., similar to sensors in situated logic programs
    . e.g., arithmetic, math, list, string operations, similar to what's in
    ISO Prolog or KIF, also extending some of XML-S datatypes capabilites for
    specializing usual basic datatypes (e.g., integer ranging 10-100)
    . could use XML-S datatypes as input-output
    . issue: might include basic capabilities for sensing/querying remotely
    over the Web, but this seems more complex and possibly problematic due
    to its dynamic nature
    o path syntax, esp. in manner of RDF Query languages' path expressions,
    and to lesser extent XPath / XQuery path expressions
    o modules
    o object-oriented argument collections
    Phase III:
    I've organized these into four groups (A,B,C,D below) of issues.
    A reasonable sequence would be to tackle them in the following order.
    But one could actually pursue them in nearly any sequence
    (there are a few dependencies).
    Group A:
    Here are some additional features which apply in the pure-belief
    logically-monotonic case, and thus also pertain straightforwardly
    to Common Logic as well:
    o modules:  i.e., named rule subsets that can be imported.
    This is a key Webizing feature.
    o object-oriented argument collections:  called "roli" in RuleML V0.8,
    often called "slots" in KR literature
    - related:  lists, both ordered and unordered
    o Lloyd-Topor And-Or:  permit AND in the head; also permit OR (nestedly
    with AND) in the body
    o sorted/typed variables and constants:  where the sort or type is
    a pure predicate/class rather than (directly and more generally/impurely)
    a programming language concrete type
    o explicit equality predicate
    o basic requests to perform inferencing
    - query -- related to DQL;
    there is a simple draft design of this in RuleML V0.8
    - "trigger":  request incremental or exhaustive forward inferencing
    - permit new rulebase premises to be sent along with the query or trigger
    o basic results of inferencing / justifications therein
    - say that a rulebase entails a set of conclusions, or
    that an engine/system/site inferred a set of conclusions from a rulebase
    - called "turnstile" in previous RuleML design discussions
    - related to DQL and DAML justifications efforts
    o Lloyd-Topor more monotonic aspects: permit existential quantifiers
    in the body, universal quantifiers in the head
    Group B:
    o rest of FOL in Common Logic:
    notably quantifiers, classical negation, equivalences.
    o This is not really rules in the LP sense, but is desirable to
    coordinate with LP rules, and is technically related to the
    Lloyd-Topor transformation feature of LP.
    Group C:
    Here are some additional features which involve non-monotonicity:
    o negation-as-failure (NAF)
    - this is particularly basic and urgent for practical rule systems
    o Courteous / prioritized conflict handling / prioritized defaults
    o selective closed-world-assumptions --
    can often, or perhaps always, be defined as a special case of NAF or Courteous
    o strong negation ("classical negation" in the limited sense used in
    extensions of LP)
    o full Lloyd-Topor transformation
    o nonmon specification of equality theory over the Herbrand universe,
    to generalize away from Unique Names Axiom;
    e.g., via prioritized defaults about explicit equality predicate
    Group D:
    o standard pure-info built-ins; supporting libraries of built-ins,
    e.g., standard ones for arithmetic, string, or list
    comparisons or operations
    - this is particularly basic and urgent for practical rule systems
    o Situated / procedural attachments:  NB:  sensing includes an
    important connection to querying and DQL
    o Events handling
    o evaluated functions:  i.e., functions that are evaluated,
    e.g., via built-in procedural attachments
    - called "nano's" in previous RuleML design discussions
    Group E:
    o Transformation rules, in formal sense of what the rules produce
    - nano's are related
    - ask Harold for more explanation
    Phase IV:
    An OWL meta-ontology of:
    - expressive features above,
    - and also of important/frequently-used restrictions, e.g.,
    . stratified use of NAF,
    . or predicates with arity of at most 2.
    % GBNF Intro, part of documents on abstract syntax specification for RuleML
    % based on draft *-v12 of that RuleML abstract syntax specification
    % by Benjamin Grosof.
    % created 3/28/03, then presented at DAML PI Meeting Rules Breakout
    % current version 4/22/03
    I. Introduction to GBNF
    Our notation for abstract syntax is called GBNF
    ("Generalized BNF for semi-structured data" or "Grosof BNF").
    GBNF is an extended variant of EBNF.
    GBNF provides a bit more detail than an EBNF specification,
    with the aim of helping to specify schemas for semi-structured data, e.g.,
    in XML-Schema and OWL/RDF.  It makes more explicit:
    - the content/children of an element;
    - unorderedness vs. orderedness;
    - attributes as a (syntactically) special kind of symbol; and
    - default values of attributes.
    GBNF statements are of three kinds: (1) ordinary production
    (a.k.a. "macro") similar to EBNF, (2) containment production, and (3)
    attribute-default.  A macro production is similar in spirit to an
    ordinary EBNF production.  A containment production specifies the
    "content" of a symbol viewed as an element in XML.  GBNF includes both
    unordered concatenation and ordered concatenation.  Attributes are
    treated as a kind of element.  An attribute-default statement
    specifies the default values for an attribute.
    The extensions of GBNF relative to EBNF are the following:
    1. containment productions (":"):
          GBNF defines a special kind of production, called a "containment",
          which expresses that the rhs of the production is intended to be
          "content" (essentially, in the XML sense) of the lhs.
          A containment production uses ":" to separate its lhs and rhs.
          A non-containment production is called a "macro".
    2. explicit indication of whether concatenation is ordered ("\") vs. unordered:
          "," in GBNF means unordered concatenation.
          "\" in GBNF means ordered concatentation.
    3. attribute-default statements:
          "myattrib $ myvalue ;" specifies that the default value of the attribute
           "myattrib" is "myvalue".
    4. attribute prefix
           In "@mysymbol", the "@" prefix indicates that "mysymbol" is an attribute
           symbol (and thus for example could have a default value).
    A GBNF specification can simply be read as EBNF,
    without fear of being misled -- simply:
    1. Interpret ":" as "=".
           (":" is a special "containment" kind of production.)
    2. Interpret "\" as ",".  Ignore every "\" before "*" or "+".
           ("\" is the ordered concatenation symbol.)
    3. Ignore every "$" statement.
           (A "$" statement's rhs defines a default value for an attribute.)
    4. Ignore every "@" prefix.
           (The "@" prefix indicates a symbol is an attribute.)
    ":" defines a containment.
    "=" defines a macro.
    "," means unordered concatenation.
    "\" means ordered concatenation.
    "|" separates alternatives (disjunctively).
    "*" means unordered Kleene star -- zero or more repetitions, concatenated.
    "?" means optional inclusion.
    "+" means one or more repetitions, concatenated and unordered.
    "(...)" delimits an expression.
    ";" delimits the end of a statement.
    "\*" is the ordered version of "*".
    "\+" is the ordered version of "+".
    "@" prefixes an attribute.
    "$" defines the default value for an attribute.
    "/* ... */" delimits a comment.
    Prof. Benjamin Grosof
    Web Technologies for E-Commerce, Business Policies, E-Contracting, Rules, 
    XML, Agents, Semantic Web Services
    MIT Sloan School of Management, Information Technology group
    http://ebusiness.mit.edu/bgrosof or http://www.mit.edu/~bgrosof

    This archive was generated by hypermail 2.1.4 : 07/08/03 EST