- From: Miles Sabin <MSabin@interx.com>
- Date: Sat, 14 Apr 2001 09:39:32 +0100
- 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 UTC