RE: RDF as a syntax for OWL (was Re: same-syntax extensions to RDF)

> -----Original Message-----
> From: www-rdf-logic-request@w3.org [mailto:www-rdf-logic-request@w3.org]
> On Behalf Of Bijan Parsia
> Sent: Wednesday, January 05, 2005 10:28 AM
> To: www-rdf-logic@w3.org
> Subject: Re: RDF as a syntax for OWL (was Re: same-syntax extensions to
> RDF)
> 
[...]
> 
> 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.
> 
> 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.

Given the challenge, I had to give it a try in RDF Gateway's rule language
;-) The results don't really rebut the ugliness claim, but do demonstrate
that it's doable in at least one of the available frameworks. BTW, I'm not
denying this was a bit of a pain, nor in any way trying to be an advocate
for the forcing of fol into rdf syntax.

I ended up with rulebase below. With it I could convert a graph to nnf form
with a few lines - e.g:

  var ds = new datasource("inet?parsetype=auto&url=c:/kill/nnftest.rdf");

  select ?p ?s ?o using #ds rulebase nnf where {[rdf:type] ?c [owl:Class]}
and nnf(?c ?p ?s ?o);

The rules may not be 100% though I tested them with a decent number of cases
(but no pathological ones). 


rulebase nnf
{
	infer nnf(?cin, ?p, ?s, ?o) from nnf_pos(?cin, ?cout, ?p, ?s, ?o);

	infer nnf_pos(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:complementOf] ?cin ?x}
		and nnf_neg(?x, ?cout, ?p, ?s, ?o);

	//	nnf(~~C)) => nnf(C)
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:complementOf] ?cin ?x}
		and nnf_pos(?y, ?cout, ?p, ?s, ?o);

	//	nnf(~(C & D)) => nnf(~C) v nnf(~D)
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:intersectionOf] ?cin ?l}
		and negateCompleteList(?l, ?cout, [owl:unionOf], ?p ?s ?o);

	//	nnf(~(C v D)) => nnf(~C) & nnf(~D)
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:unionOf] ?cin ?l}
		and negateCompleteList(?l, ?cout, [owl:intersectionOf], ?p
?s ?o);

	//	nnf(~some(P, C)) => all(P, nnf(C))
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:onProperty] ?cin ?prop}
		and {[owl:someValuesFrom] ?cin ?svc}
		and ?cout=newid()
		and	nnf_pos(?svc, ?svcout, ?a ?b ?c)
		and (
				statement(?a ?b ?c ?p ?s ?o)
					or
				statement([owl:onProperty] ?cout ?prop ?p ?s
?o)
					or 
				statement([owl:allValuesFrom] ?cout ?svcout
?p ?s ?o)
			);

	//	nnf(~all(P, C)) => some(P, nnf(C))
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from isAnon(?cin)
		and {[owl:onProperty] ?cin ?prop}
		and {[owl:allValuesFrom] ?cin ?vc}
		and ?cout=newid()
		and	nnf_pos(?vc, ?vcout, ?a ?b ?c)
		and (
				statement(?a ?b ?c ?p ?s ?o)
					or
				statement([owl:onProperty] ?cout ?prop ?p ?s
?o)
					or 
				statement([owl:someValuesFrom] ?cout ?vcout
?p ?s ?o)
			);

	//	nnf(C) => C
	infer nnf_pos(?cin, ?cout, ?p, ?s, ?o) from instr(?cin, 'guid') <> 0
and
		?cout=?cin and ?s=?cin and {?p ?s ?o};

	//	nnf(~C) => ~C
	infer nnf_neg(?cin, ?cout, ?p, ?s, ?o) from instr(?cin, 'guid') <> 0

		and ?cout=newid() 
		and (
				(?s=?cin and {?p ?s ?o})
					or
				statement([owl:complementOf] ?cout ?cin ?p
?s ?o)
			)

	//helpers
	infer negateCompleteList(?l, ?cout, ?pred, ?p, ?s, ?o) from
?newlist=newid()
		and ?cout=newid()
		and (
				negateList(?l, ?newlist, ?p ?s ?o)
					or 
				statement([rdf:type] ?cout [owl:Class] ?p ?s
?o)
					or 
				statement(?pred ?cout ?newlist ?p ?s ?o)
			);

	infer negateList(?l, ?newlist, ?p ?s ?o) from {[rdf:first] ?l
?first}
			and {[rdf:rest] ?l ?rest}
			and switch(?l)
				(
				case ?rest=[rdf:nil]:
					?newrest=[rdf:nil]
				default:
					?newrest=newid()
				)
			and	nnf_neg(?first, ?firstout, ?a ?b ?c)
			and (
					statement(?a ?b ?c ?p ?s ?o)
						or
					statement([rdf:first] ?newlist
?firstout ?p ?s ?o)
						or 
					statement([rdf:rest] ?newlist
?newrest ?p ?s ?o)
						or 
					negateList(?rest ?newrest ?p ?s ?o)
				);

	infer statement(?pin ?sin ?oin ?pout ?sout ?oout) from ?pout=?pin
and ?sout=?sin and ?oout=?oin;
	infer isAnon(?x) from instr(?x, 'guid') = 0;
}

 
> Actually, just trying stating the rules using RDF triples in your
> favorite syntax.
>
> Cheers,
> Bijan Parsia.

Rgds,

Geoff Chappell

Received on Thursday, 6 January 2005 03:07:59 UTC