Re: Inconsistency in DAML+OIL Axiomatic Semantics

Miles Sabin wrote:
> 
> Ken Baclawski wrote,
> > 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)))))
> 
> Unless I'm missing something this is equivalent to the original.
> All of s, v1, and v2 are free in the LHS of the conjunction and
> in the LHS of the biconditional, so the forall can be pushed to
> the outermost scope. Then it can be dropped altogether because
> KIF treats free variables in quantifier free sentences as
> implicitly universally quantified.

That universal quantifiers can be pushed out is true
as a rule of thumb, but it doesn't always apply in the "if" part
of a conditional. That is:

	(=> (=> (in ?x ?set) (inOrder ?y ?x))
            (min ?set ?y))

is very different from

	(=  (forall (?x)
		(=> (in ?x ?set) (inOrder ?y ?x)) )
            (min ?set ?y))



> Can you give a sketch of the generated proof that all properties
> are functional and the role that this axiom plays in it?

Given the original formulation of the axiom...

 (<=> (Type ?fp FunctionalProperty) 
          (and (Type ?fp Property)
               (=> (and (PropertyValue ?fp ?s ?v1) 
                        (PropertyValue ?fp ?s ?v2))
                   (= ?v1 ?v2))))

Take any old property... say... rdf:type
and any of its subject/object pairs... say
Adam and Person. Then we have
	(Type rdf:type Property)
of course and we have
	(= Person Person)
and
	(and (PropertyValue rdf:type Adam Person)
	     (PropertyValue rdf:type Adam Person))
now we can conclude
	(=> (and (PropertyValue rdf:type Adam Person)
	     (PropertyValue rdf:type Adam Person))
            (= Person Person))
from which we can conclude
	(Type rdf:type FunctionalProperty)

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Saturday, 14 April 2001 09:29:34 UTC