From: Harold Boley (firstname.lastname@example.org)
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