W3C home > Mailing lists > Public > www-rdf-logic@w3.org > April 2001

Re: Inconsistency in DAML+OIL Axiomatic Semantics

From: Dan Connolly <connolly@w3.org>
Date: Fri, 13 Apr 2001 22:58:09 -0500
Message-ID: <3AD7CAD1.356EB053@w3.org>
To: Ken Baclawski <kenb@ccs.neu.edu>
CC: www-rdf-logic@w3.org
Ken Baclawski wrote:
> 
> The UBOT project has been examining the consistency of the
> DAML+OIL axiomatic semantics. Using an automated theorem
> prover, Richard Waldinger found an inconsistency due to
> Axiom 8.  This axiom is the following:
> 
> Ax8. (<=> (Type ?fp FunctionalProperty)
>           (and (Type ?fp Property)
>                (=> (and (PropertyValue ?fp ?s ?v1)
>                         (PropertyValue ?fp ?s ?v2))
>                    (= ?v1 ?v2))))
> 
> >From this axiom one can conclude that every property is
> functional.

Oops!

>  As there are many properties that are not
> functional (such as type), this leads quickly to logical
> inconsistencies in the axiomatic semantics.
> 
> We suggest that this axiom be changed to:
> 
> Ax8. (<=> (Type ?fp FunctionalProperty)
>           (and (Type ?fp Property)
>                (forall (?s ?v1 ?v2)
>                   (=> (and (PropertyValue ?fp ?s ?v1)
>                            (PropertyValue ?fp ?s ?v2))
>                       (= ?v1 ?v2)))))

Yup... I think that's what we meant.

I'm interested in more details about the technology
you used to find this bug. Where can I read more
about it?

How did you get the axioms into the prover? does
it read KIF?

I was hoping we'd provide the KIF stuff in raw
form, but we didn't get around to it.
Did you extract them manually? Did you have
to translate them to some other syntax?

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Friday, 13 April 2001 23:58:14 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT