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

RE: Inconsistency in DAML+OIL Axiomatic Semantics

From: Miles Sabin <MSabin@interx.com>
Date: Sat, 14 Apr 2001 09:39:32 +0100
Message-ID: <69B15B675E99D411A4110008C786DA23DED96E@exwest_01.interx.com>
To: www-rdf-logic@w3.org
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.

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

Cheers,


Miles

-- 
Miles Sabin                               InterX
Internet Systems Architect                5/6 Glenthorne Mews
+44 (0)20 8817 4030                       London, W6 0LJ, England
msabin@interx.com                         http://www.interx.com/
Received on Saturday, 14 April 2001 04:40:17 GMT

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