- From: Dan Connolly <connolly@w3.org>
- Date: Fri, 13 Apr 2001 22:58:09 -0500
- 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 UTC