A problem with HasKey in the functional-style syntax

Hello,

I've just noticed a problem in the functional-style syntax for HasKey. The
current syntax is

HasKey( CE P1 ... Pn )

where Pi are either object or data properties. But this means that the axiom is
not fully typed. Consider, for example, the following axiom:

HasKey( a:MyClass a:MyProperty )

>From this axiom alone, it is not clear whether a:MyProperty is an object or a
data property. Effectively, this means that we haven't addressed correctly the
comment by Matthew Horridge.

My proposal for fixing this is to write the above axiom like this:

HasKey( a:MyClass ObjectPropertyList( a:MyProperty ) )

More generally, the grammar would be like this:

HasKey := 'HasKey' '(' ClassExpression
    'ObjectPropertyList' '(' { ObjectPropertyExpression } ')' |
    'DataPropertyList'   '(' { DataPropertyExpression   } ')'
')'

This change should be propagated to all the other documents as well.

Unless someone objects, I'll make this change tomorrow afternoon.

Regards,

	Boris

Received on Wednesday, 18 March 2009 17:38:21 UTC