- From: <jos.deroo@agfa.com>
- Date: 06-Jan-2005 02:00:46 CET
- To: bparsia@isr.umd.edu
- Cc: www-rdf-logic@w3.org
Hi, Bijan Saw your reply (and scraped it from) http://lists.w3.org/Archives/Public/www-rdf-logic/2005Jan/0019.html i.e. I didn't receive recent messages from www-rdf-logic@w3.org > On Jan 5, 2005, at 11:29 PM, jos.deroo@agfa.com wrote: > >> Yes, but we do OWL/RDF/XML<->RDF/N3 automatically (using >> Jena2 or Cwm) and then just *add* explicit theories such as >> e.g. the ones in http://eulersharp.sourceforge.net/#theories > > Would you be comfortable using such a theory as a specification for the > semantics of OWL? (Pace minor bugs, natch.) No, not in this edition; it is fairly incomplete and was mainly done as an effort to test OWL test cases. I look forward to many improvements, such as N3 cnf/nnf/.. rewriters (like the challenge you pose in this message), class and property equality inferencing support, etc.. >> Indeed, the latter is still a matter of "selecting by human". >> At this moment RDF/N3<->TSTP transcription is semiautomatic >> and is why I will have to come back later when I have more >> running code to sharply illustrate what I found feasable :) > > Jos, I have a way way easier challenge: do the negation normal form > transformation > > Specification: Given an input graph, produce an output graph such that > all negations appear only on class names in a class expression. > > Actually, let's make it even easier! Only for ALC > > I'll even give the rules: > I'll use ~ for not (complementOf) > & for conjunction (intersectionOf) > v for disjunction (unionOf) > some for existential quantification (someValuesFrom) > all for universal quantification (allValuesFrom) > I'll use fairly normal infixy syntax. I'll happily convert to > something else. > > For (compound) class expressions C and D > nnf(~~C)) => nnf(C) > nnf(~(C & D)) => nnf(~C) v nnf(~D) > nnf(~(C v D)) => nnf(~C) & nnf(~D) > nnf(~some(P, C)) => all(P, nnf(C)) > nnf(~all(P, C)) => some(P, nnf(C)) > > Base case: for atomic class name C > nnf(C) => C > nnf(~C) => ~C > > That's almost the prolog program :) > > I'll accept the binary restriction on & and v. OK, I see, but we actually do rewrites, adding comprehension axioms, etc (using Java or C# code) before we start RDF/N3 based triple inferencing (such as to run positive entailment tests, inconsistency tests, q:select's etc...) and so your excercise can only inspire my Java or C# code :) > To make it easier, I'll allow for the class expressions to be isolated > (i.e., not part of an axiom), if that helps. > > I believe this exercise will be illuminating to anyone who tries it. > > Actually, just trying stating the rules using RDF triples in your > favorite syntax. > > Cheers, > Bijan Parsia. -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 6 January 2005 01:01:25 UTC