Re: AW: Safe Execution of Recursive Axioms + English

On Tue, 7 Oct 2003, Enrico Franconi wrote:

> On Thursday, Oct 2, 2003, Raphael Volz wrote:
> > indeed Ian Horrocks, Benjamin Grosof, Stefan Decker and me
> > have shown (in the Description Logic Program paper at WWW)
> > that you can NOT implement SHIF (the DL below
> > OWL Lite) via Datalog, but a (more or less - depending on your
> > own perspective) fragment thereof.
> 
> Well, this can be proved by simple complexity arguments (poly vs  
> EXPTIME-hard).

That is a feasible alternative way. However, our translation additionally 
gives you an LP-encoding for the fragment that can be translated.

> 
> > One example is existential quantification, which you can
> > only do in one directions of implication, since existentials
> > in the head are generally unavailable in Datalog. Another
> > example is negation, which has different semantics (incompatible
> > with FOL negation).
> 
> Your work contains an obvious and trivial polynomial fragment of OWL,  
> known since long time, whose impact in the real ontology world has to  
> be empirically shown yet. Its impossibility to freely intermix  

I think, that really depends on ones' subjective standpoint. If you
look at the ontologies in the DAML library a great number falls into
our "useless" fragment. I guess, that many SemWeb ontologies, given that 
they are constructed by ordinary people and not expert logicians, will
fall into our subset, for which - polynomial by nature - you will at least
have realisitc (scalable) A-Box support, which is absent for the 
expressive DLs underlying OWL.

> universal and existential quantifiers makes it, to my opinion, quite  
> useless.
> 
> > I believe that you - generally - can NOT implement OWL Lite
> > with rule-based reasoners.
> 
> It is not only a belief, you can formally prove it! No sub-boolean DL  
> (e.g., FL-) with full axioms, and no DL with full booleans (e.g. ALC)  
> without axioms can be ever encoded in a polynomial language (e.g., a  
> rule-based reasoner), as a matter of fact.

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. 
> 
> > 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  
> (with a complexity coming either from full axioms or from the booleans)  
> can be ever be encoded in it. This is the case of OWL-lite which is  
> EXPTIME-hard. So, again, I don't understand what are you really doing.
> 
Boris Motik is working on the proof, we will see if he can proof it or 
not.

> Passing the test in the OWL Test Suite does not seem to me anything  
> like a soundness and completeness proof for any algorithm. I wonder  
> which other tests did your system pass. Did you consider the standard  
> DL test suite (e.g. see http://www.dis.uniroma1.it/~tancs/ or  
> http://kogs-www.informatik.uni-hamburg.de/~moeller/dl-benchmark- 
> suite.html)?

Some of these tests have been taken into the OWL Test Suite, we will
work further on the formal proof. We will later try these (other) test 
suites. But you are right, passing a test suite does not really proof
soundness and completeness.

R.


> 
> cheers
> --e.
> 
> Enrico Franconi                  - franconi@inf.unibz.it
> Free University of Bozen-Bolzano - http://www.inf.unibz.it/~franconi/
> Faculty of Computer Science      - Phone: (+39) 0471-315-642
> I-39100 Bozen-Bolzano BZ, Italy  - Fax:   (+39) 0471-315-649
> 

-- 

Raphael Volz
Institut AIFB
Uni Karlsruhe(TH)

Tel:  +49 (721) 608 7363
Mail: volz@aifb.uni-karlsruhe.de

Received on Tuesday, 7 October 2003 08:17:05 UTC