Re: Inconsistency in DAML+OIL Axiomatic Semantics

On Fri, 13 Apr 2001, Dan Connolly wrote:

> 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?

We are using several technologies.  The ConsVISor tool
integrates model-checking and theorem-proving.  It is
one of the tools in the UBOT toolset.  The theorem
prover used by ConsVISor is SNARK.  For information
about SNARK see <www.ai.sri.com/~stickel/snark.html>.
The UBOT Web site is <ubot.lockheedmartin.com>.

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

Yes, it does 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?

It was extracted manually.  We added names to the axioms
to make them more readable during theorem proving (see below).
We also added a number of "obvious" missing axioms such as the
fact that Alt is a Class.

Here is the refutation of Axiom 8.  
SNARK very quickly deduced that type is a functional property
and that Alt is both a Class and a Resource, contradicting the
fact that type is functional.  Notice the KIF notation in the
refutation.

(Refutation
 (Row type-is-property-Ax16.6
      (Type type Property)
      assertion)
 (Row alt-is-classProblems-Document.10
      (Type Alt Class)
      assertion)
 (Row properties-are-not-classes-Ax7.21
      (or (not (Type ?Element Property))
   (not (Type ?Element Class)))
      assertion)
 (Row type-vs-propertyvalue-Ax1.29-48
      (or (not (Type ?Element ?Element1))
   (PropertyValue type ?Element ?Element1))
      assertion)
 (Row definition-of-functional-property-Ax8.19-49
      (or (Type ?Element FunctionalProperty)
   (not (= ?Element1 ?Element2)))
      assertion)
 (Row definition-of-functional-property-Ax8.19-52
      (or (not (Type ?Element FunctionalProperty))
   (not (Type ?Element Property))
   (not (PropertyValue ?Element ?Element1 ?Element2))
   (not (PropertyValue ?Element ?Element1 ?Element3))
   (= ?Element2 ?Element3))
      assertion)
 (Row arguments-of-type-Ax17.5-61
      (or (not (Type ?Element ?Element1))
   (Type ?Element Resource))
      assertion)
 (Row 70
      (not (Type type Class))
      (resolve properties-are-not-classes-Ax7.21
type-is-property-Ax16.6))
 (Row 92
      (Type ?Element FunctionalProperty)
      (resolve definition-of-functional-property-Ax8.19-49 code-for-=))
 (Row 93
      (or (not (Type ?Element Property))
   (not (PropertyValue ?Element ?Element1 ?Element2))
   (not (PropertyValue ?Element ?Element1 ?Element3))
   (= ?Element2 ?Element3))
      (rewrite definition-of-functional-property-Ax8.19-52 92))
 (Row 120
      (PropertyValue type Alt Class)
      (resolve type-vs-propertyvalue-Ax1.29-48
alt-is-classProblems-Document.10))
 (Row 394
      (Type ?Element Resource)
      (resolve arguments-of-type-Ax17.5-61 92))
 (Row 406
      (PropertyValue type ?Element Resource)
      (resolve type-vs-propertyvalue-Ax1.29-48 394))
 (Row 407
      (or (not (PropertyValue type Alt ?Element))
   (= Class ?Element))
      (rewrite (resolve 93 120) type-is-property-Ax16.6))
 (Row 604
      (= Class Resource)
      (resolve 407 406))
 (Row 637
      false
      (rewrite (paramodulate 70 604) 394))
 )

Ken Baclawski
UBOT Project
College of Computer Science
Northeastern University

Received on Saturday, 14 April 2001 10:40:34 UTC