AW: AW: Safe Execution of Recursive Axioms + English

> > I would like to stay with my belief, you may choose to do some
> > preprocessing and compile things and later use your polynomial language
> > to do the rest.
>
> I don't get your point. A proof is stronger than a belief :-)

I got your point, no one says that what the preprocessor does necessarily
has to be tractable.

>
> > > > What you seems to be possible
> > > > is using Disjunctive Logic Programs, but our proof that an
> > > > appropriate translation is indeed correct is not quite finished
> > > > yet. Empirically, we pass all tests in the OWL Test Suite and
> > > > other well-known DL tests.
> > >
> > > Still, DLP in its full power is below PSPACE, so again no
> reasonable DL

Of course, the data complextity of DLP is Sgima-Pi-2, so it is still in the
polynomial hierarchy, but it is Nexptime^NP-complete in the program size. We
a working on a
reduction of SHIQ to Disj. Datalog with equality, (w/o closed world negation
!)
which will for some knowledge base generate a set of rules (whose number is
worst-case exponential in the size of the knowledge base), which preserves
satisfiabilty and entailment. You may contact Boris (motik@fzi.de) to ask
further questions and/or
take his proof apart.

Sincerely yours

R.