A Model-Theoretic Semantics for DAML+OIL (March 2001) (original) (raw)
IO(?O) <= IC(?C)
rdf:type,?O,?D rdf:value,?O,?L rdf:type,?L,rdfs:Literal
for ?D an XML Schema datatype,IO(?O) is the singleton set containing the element ofIC(?D) that has lexical representation ?L, provided that there is one, otherwise IO(?O) = { }
in IR(?R), for some x <=IO(?O1) and y <= IO(?O2), provided that IO(?O1) <= AD IC(?A) = IC(?B) IR(?A) = IR(?B) IO(?A) = IO(?B) IC(?C) <= IC(?D) IR(?R) <= IR(?S) IC(?C) = IC(?D) IR(?R) = IR(?S) IO(?A) = IO(?B) IC(?X) ^ IC(?Y) = { } IO(?A) ^ IO(?B) = { } IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD IC(?Xi) ^ IC(?Xj) = { } for 1<=i IC(?C) = IC(?X1) ^ ... ^ IC(?Xn) ^ AD IC(?X) ^ IC(?Y) = { } IC(?X) v IC(?Y) = AD IC(?C) = ( IO(?O1) v ... v IO(?On) ) ^ AD if in IR(?P) then x in IC(?C) if in IR(?P) then y in IC(?C) for y in AD, in IR(?P) iff in IR(?S) for y in AD, if in IR(?P) and in IR(?P) then in IR(?P) if in IR(?P) and in IR(?P) then y=z for y in AD, if in IR(?P) and in IR(?P) then x=z x in IC(?R) iff IR(?P)({x}) <= IC(?C) x in IC(?R) iff | IR(?P)({x}) ^ IO(?V) | > 0 x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0 x in IC(?R) iff | IR(?P)({x}) | >= ?n x in IC(?R) iff | IR(?P)({x}) | <= ?n x in IC(?R) iff | IR(?P)({x}) | = ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n x in IC(?R) iff IR(?P)({x}) <= IC(?C) x in IC(?R) iff | IR(?P)({x}) ^ IC(?V) | > 0 x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0 x in IC(?R) iff | IR(?P)({x}) | >= ?n x in IC(?R) iff | IR(?P)({x}) | <= ?n x in IC(?R) iff | IR(?P)({x}) | = ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n