Equality Hubs

From: Harold Boley (boley@informatik.uni-kl.de)
Date: 07/01/03

  • Next message: Benjamin Grosof: "comments invited: draft of axiomatization of explicit equality for LP rules language"
    Hi JC Colleagues,
    
    in today's JC telecon we came back to the topic of equality in ontology (OWL) and rule (RuleML) languages.
    Since unrestricted reasoning with equality (http://cbl.leeds.ac.uk/nikos/pail/logic/section3.8.html)
    in the sense of Paramodulation is hard, pre-Web researchers have suggested directed versions of equality:
    (Ground) Rewriting and (Non-Ground) Narrowing -- see e.g. the summary in Sergio Antoy's recent introductory
    slides at http://www.cs.pdx.edu/~antoy/Courses/TPFLP/lectures/NARROWING/narrowing.pdf.
    
    When I suggested to look at such 'directed equality' and 'canonical name' work, Pat pointed out this is hard
    to realize on the Web, since new individual names can come in at any time, so that -- as I then put it --
    "You never know if you are (still) a normal form".
    
    However, it now seems to me that "Equality Hubs" will emerge in the Web, much like a special kind of Google's
    Hyperlink Hubs. When some community at http://www.c1000.org discovers that their individual n is the same as
    what some other community at http://www.c0001.org has already defined as the individual m, an equality link
    n --> m from c1000's n to c0001's m is likely to be created without c0001 being aware of, or interested in,
    the possibility of creating a symmetric link m --> n. Similarly, further communities may create n' --> m,
    n'' --> m, ... without lots of inverse (from m to some n) or 'horizontal' links (between some n's). This way,
    http://www.c0001.org is becoming an Equality Hub for the quasi-canonical name m with many directed equalities
    linking into it. Moreover, some of the sites defining n's may become Equality Subhubs, etc., in a mostly
    tree-like manner. As we discussed, for any individual a new quasi-canonical name and Equality Hub may emerge
    over time, providing a new 'root' to which most of the sites and subhubs will redirect their equalities.
    
    But circular equality links such as the mutually horizontal link n' <--> n'' will also emerge, so that the
    hub structure alone does not provide a trivial name normalization algorithm that would "just follow the links
    up to the root": Like in normal hub discovery, equality hub algorithms must provide for loop detection to cut
    off any circular paths. Still, augmented by Equality Hub detection and maintenance, the above-mentioned/linked
    techniques of directed equality should be useful for Web KR.
    
    Best,
    Harold
    
    
    PS: Explicit equality is also provided in RuleML 0.8 (the 'eq' element).
    
    Definition:
    http://www.ruleml.org/dtd/0.8/ruleml-equalog.dtd
    
    Examples:
    http://www.ruleml.org/exa/0.8/uriexp.ruleml
    http://www.ruleml.org/exa/0.8/factorial.ruleml
    
    However, we are now working on the more computational tractable
    directed equality to complement (or possibly, replace) 'eq':
    
    A transformation-rule extension is in the RuleML 0.81 prerelease.
    Here are the still incomplete transformation rule DTDs/examples:
    http://www.ruleml.org/indtd0.81.html (forthcoming soon)
    http://www.ruleml.org/dtd/0.81/ (available now)
    http://www.ruleml.org/exa/0.81/ (available now)
    
    
    PPS: http://www.ruleml.org/... --> http://www.dfki.uni-kl.de/ruleml/...
    is usually done automatically  --  sorry if this 'normalization' is
    temporarily broken; it will be fixed ASAP.
    


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