[SCL] naming ontologies

[pat hayes]

Guys, that idea of 'headers' has morphed into a slightly more general 
idea. Let me try this out on everyone to see how it flies.

First, observe that there is a need to provide a way to give a name 
to an ontology for use on the Web, and it ought almost certainly to 
be a URI.  So suppose that we provide for some simple syntax for 
naming a set of sentences by attaching a URI to the sentences: I'll 
write this as a URI enclosed in angle brackets followed by  a list of 
SCL sentences enclosed in double square brackets, but we can 
obviously do better in say, XML.

The meaning of this notation is that the name denotes this set in all 
satisfying interpretations: this requires that the universe admits 
things called 'sets of sentences' which as far as the semantics are 
concerned can be thought of simply as functions from interpretations 
to truthvalues, i.e. as propositions, which we can treat as a 
primitive semantic category (like strings and integers). So if 
'ex:ont' is such a URI then it makes sense to write something like 
I(J('ex:ont')) = true where I and J are SCL interpretations.

Ontology names like this can then be used to import one ontology into 
another, so that an SCL document named ex:A can contain a top-level 
sentence 'import ex:B' indicating that any satisfying interpretation 
of A is required to satisfy all the sentences in  B. This is emerging 
semantic-web practice (it corresponds to the owl:imports definition) 
and it seems to be generally useful, e.g. it provides a neat way to 
import 'standard' axiom sets or concept definitions.

Given this, however, we have a new option, which is to attach a name 
to an ontology *inside another ontology*.  This can be used together 
with a variation of the 'header vocabulary' to give a general-purpose 
way of describing implicit contexts (such as the assumed syntactic or 
semantic restrictions on various symbols) as enclosing SCL 
surrounding, but not included in, an ontology naming.  This requires 
a special semantic condition analogous to the 'header' condition: if 
we perform an 'inner' labelling, as in:

[[ outer sentences <ex:inner>[[ inner sentences]] ...]]

then I satisfies ex:inner just when it satisfies the inner sentences 
*and some extension J of I satisfies the outer sentences*  where, as 
before, the special header vocabulary Ind, Rel etc, refers to the 
constructs in I rather than J (this follows automatically since we 
are talking about I as the satisfying interpretation, but it might be 
worth emphasizing).  We could call this a 'contextual' labelling. 
Note that a simple outer-level labelling can be described as a 
contextual labelling with a trivially true context.

For example:

<ex:outer>[[
(Ind  a)
(Rel  P) (Rel Q)
(Arity  ?n  P) iff (= ?n 1)
	<ex:inner>[[
	(forall (?x) (= ?x a))
	(P a)
	(not (Q a))
	]]
]]

defines two SCL ontologies.  Here, ex:inner is SCL-satisfiable in a 
FO Herbrand interpretation with universe {a}, ext(P)={<a>}, 
ext(Q)={}, even though in this (Horrocks) case there is no SCL 
interpretation which satisfies all the inner and outer sentences 
simultaneously. The 'contextual' assertions outside the labelled 
ontology are not required to be made true by interpretations of the 
ontology, since they may mention entities which do not exist in those 
interpretations, but they are required to be satisfied in a less 
direct sense: one might say, it must always be *possible* that they 
could be true, in a rather strong sense of 'possible' (if you were to 
allow that some other things exist, then they could become true.) 
Note that the enclosing outer ontology in a case of contextual 
definition like this has to be given a special status as part of the 
definition of the inner labelling.

We havn't yet said what it means to satisfy ex:outer, but I propose 
that it would be satisfiable for example by J with a Herbrand 
universe {a, P, Q, Ind, Rel, 1, pr} and J(ex:inner)=pr and 
J(pr)=false. That is, the outer ontology is required to respect the 
labelling, but it isn't required to *satisfy* the inner ontology. 
The inner 'naming' is rather like a quotation in this respect.  This 
means that it would be OK to import either ex:inner or ex:outer, but 
if you import them both then you are SCL-inconsistent (and if you 
import the outer, then you cannot subsequently disagree about the 
meaning of 'ex:inner'; but since that is a URI one would not expect 
that you would be able to disagree about it in any case.)

Note that any importation of the inner ontology has to carry along 
the satisfaction conditions of the outer part of the contextual 
labelling. In practice this will mean that it is unwise to import 
ontologies defined from different contexts into a single ontology, 
unless you *really* know what you are doing; which in turn means that 
many contextual definitions will probably have a special form:
[[(import <standardOuterOntology>) .... ex:newOntology[[....]] ]]
where the context is simply a reiteration of a 'standard' form of 
some kind, perhaps with some special additions for the particular 
vocabulary.  We can provide some of these ourselves, eg a generic 
GOFOL outer ontology form. Also, in the XML syntax we can provide for 
an abbreviated version of this format since it is so likely to be 
widely used.

The previous 'header' idea appears now as the header being simply an 
enclosing ontology. I feel this is more elegant and simpler than 
having a special syntactic distinction between body and header, and 
it integrates nicely with the 'ontology-labelling' idea which we need 
to provide in any case in a working language for interchange.  It 
also makes the transition into a simple ontology more obvious. The 
ontology gotten by erasing the inner labelling and just dumping all 
the sentences into a single ontology is SCL unsatisfiable (since P 
and Q appear as arguments so must be in the universe and must be 
distinct):  the 'inner' sentences can be moved to the 'outer' 
ontology without change of meaning only provided that all quantifiers 
are restricted to the 'inner' universe Ind. Call the result ex:flat:

ex:flat[[
(Ind  a)
(Rel  P Q)
(Arity  ?n  P) iff (= ?n 1)
(forall (?x) (implies (Ind ?x) (= ?x a)) )
(and (Ind a) (P a) )
(and (Ind a) (not (Q a)) )
]]

then ex:flat is SCL satisfiable; indeed, every satisfying 
interpretation of it has a sub-interpretation which satisfies 
ex:inner, and vice versa. And of course this is a general result for 
any pair of inner and outer ontologies: and it allows for further 
layering if required, so that ontologies can be 'nested' inside one 
another in any combination.

Sorry this seems to be constantly changing, but really there is a 
single idea here, and the changes are consequences of trying to 
explain it as simply as possible and trying to absorb as much of the 
variation as possible into the model theory rather than the syntax.

Any comments welcome.

Pat

PS. There might still be a role for a 'header', but now it would 
really be purely syntactic, eg as a standard way to identify which 
SCL concrete syntax was being used in the document. For this kind of 
purpose I would be quite happy to restrict this to XML, thereby 
acknowledging that the XML surface form has a special status for 
document interchange and is the only truly 'universal' format for SCL 
transmission.
-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes