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: Sat, 14 Apr 2001 08:29:30 -0500
Message-ID: <3AD850BA.93D013A5@w3.org>
To: Miles Sabin <MSabin@interx.com>
CC: www-rdf-logic@w3.org
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 GMT

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