looking at description logics

While looking at description logics we found lots of Euler circuits ...

Example 1: person subsumes parent

  person(X):- parent(X).

  parent(X):- person(X), has-child(X,Y), person(Y).

Example 2: animal AND biped subsumes human

  animal(X):- human(X).

  biped(X):- human(X).

  human(X):- animal(X), biped(X), ...

Example 3: human AND female defines woman

  human(X):- woman(X).

  female(X):- woman(X).

  woman(X):- human(X), female(X).

Example 4: conceptC equiv conceptD

  conceptC(X):- conceptC(X).

  conceptD(X):- conceptC(X).

If for example 4 we also assert conceptD("a") and conceptC("b")

so that we have http://www.agfa.com/w3c/euler/equiv.axiom.rdf

then conceptC("a") http://www.agfa.com/w3c/euler/equiv.lemma.rdf

is proved non-empty at http://www.agfa.com/w3c/euler/equiv.proof.rdf

If we indeed have Euler circuit detection to stop looping around,

then http://www.agfa.com/w3c/euler/ is working for such examples.

Are there any issues that we should think about?

--

Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/