Re: terminating 'imports' loops

From: pat hayes (
Date: 03/22/01

>pat hayes wrote:
> >
> > I suggest adding the following sentence to the end of the paragraph
> > in the ref manual.
> > Comments? re-wordings?
>I could live with that specification, but I wonder...
>do you really want to use the same term for 'imports'
>and its transitive closure?

Well, thats what the refmanual says right now, I was just closing any 
transitive loops. But more generally, I think that it makes sense for 
importing to be transitive. After all, if B imports A it presumably 
means to assert everything in A, and so if C imports B then it needs 
to assert averything which B asserts which has to include everything 
that A asserts...and so on.

>While I've got your attention on this
>subject... I think I first ran into it
>as 'Assertion of another document'
>in TimBL's semantic web toolbox.
>In my attempts to formalize it,

Ah. I wouldnt try to formalise it in the assertional language itself, 
since its really about the process of making assertions rather than 
about truth. Appended below is a draft of a proposal I made for 
modifying KIF to allow explicit importing. The ad-hoc KIF committee 
were, er, lukewarm about it. I think the naysayers are of the view 
that KIF shouldnt even be dealing with nasty un-logical issues like 
this, which I think is like saying that one is going to ignore 
freeways: a noble stance to take, but doomed.

BTW if y'all have any comments on this, I'd be delighted to hear 
them. especially if they are negative :-)

Back to your message:

>I've always done
>so by way of something list ist from context logic; or
>maybe it's something like the entails/gate thingy:
>  (forall (?ont1 ?ont2 ?f)
>	(=>
>          (and (sw:entails ?ont1 ?f)
>	       (daml:imports ?ont2 ?ont1))
>          (entails ?ont2 ?f)
>        ))

I mean, it ought to be the case that if A imports B then that is kind 
of like copying B into A (with appropriate caveats about namespace 
conventions using #) , and so if we set out to say what difference 
having B copied into it ought to make to A, it would be that anything 
that would be entailed by (#A+ B) should also be entailed by B when 
it includes A, where #A means something just like A but with '<A's 
URI>#' written in front of all its names. Now, to state this 
namespace convention in something like KIF, it would have to be able 
to describe its own lexical items, which is the part of new-KIF that 
we havnt got to yet, but there doesnt seem to be any insuperable 
barrier to having it able to do that.

BUt once that can be done, then I think the transitivity rule can be 
stated just using good old implication, ie it would look something 
like this:

(=> (=> B (imports foo A)) (=> (=> A baz) (=> B (wtr (prefixname foo# baz)))))

where (prefixname x y) indicates the expression got from y by doing 
that name-prefixing operation, and then you have to dereference it 
with wtr to get the content back. But the point is that we don't need 
to say what is IN an ontology, only what that ontology IMPLIES.

This is highly sketchy, of course.

>where entails is built on some kind of says thingy:
>  (forall (?doc ?f1 ?f2)
>    (=> (and (sw:says ?doc ?f1)
>             (wtr ^(=> ,?f1 ,?f2)) )
>        (sw:entails ?doc ?f2) ) )
>but of course this binds sw:entails very closely
>with KIF wtr and such... which brings up
>all those KIF annoyances about using variables
>in the syntactic place where predicates go and
>such... you're working on fixing that, aren't
you Pat? Any news?

Chris Menzel and I are working hard on a full draft spec for the new 
KIF. We have all the technical work done, but writing it up in a form 
which is both readable and satisfies all the other IEEE/KIF-community 
agendas is quite a task. For an excellent summary and extended 
examples see

The new KIF syntax will certainly allow one to put a variable 
anywhere, including in relation or function position in any 
expression or term, so you can quantify over relations and functions. 
You won't be able to quantify over connectives or actual quantifiers, 
is about the only restriction; and one can even define relations that 
combine other relations in connective-like ways, eg  'union' , 
defined by the following new-KIF axiom:

>(forall (?r1 ?r2 (relation ?c1) (relation ?c2))
>       (forall (@args)
>               (<=> ((union ?r1 ?r2) @args)
>                    (or (?r1 @args)
>                        (?r2 @args)))))

The @ means a 'row variable' (formerly 'sequence variable'), ie it 
stands for any sequence of arguments; so this works for relations of 
any arity. All this, and still first-order! (Actually if you are too 
free with @ you go outside strict first-order, but only a wee bit. 
The above example is OK.)

>I'm aware of a few other approaches that might
>work, but they seem to use
>higher order logic: McDermott's lambda
>and the PCA stuff.

I still havnt fully absorbed PCA yet.
Heres the KIF namespace proposal: Again, please don't circulate this widely.

Namespaces and inclusion

An ontology (traditionally called a 'theory' in logic) is a set of 
assertional expressions. Each ontology has an associated vocabulary 
or namespace, defined to be all the identifiers used in its 
expressions, other than those with a predefined logical meaning.  A 
KIF ontology can be given a name, which can be indicated in KIF  by 
enclosing all the expressions of the ontology, preceded by the word 
"ontology" and the name itself, within parentheses. Such an 
expression is called an ontology form. (We use this label, rather 
than "expression",  since the form does not denote anything, but 
indicates a set of axioms by ostention.) Such a name of the ontology 
is considered to be part of the ontology namespace, so must be 
distinct from other symbols in that namespace; it is called a local 

Other methods for giving names to ontologies are acceptable. In 
particular, the ontology may reside on a web page, or in a computer 
file, in which case the URI of the page, or the name of the file, may 
be used as names for the ontology (provided they are KIF lexical 
items. They can usually be made acceptable by inserting backslashes 
in front of any interlexical characters.) These are intended to have 
a scope which extends beyond the ontology itself, so are called 
global names.  KIF assumes that some external process is capable of 
accessing the ontology named by a global name, so the exact form of 
global names is not mandated by the KIF standard.  Some convention 
should be establsihed which guarantees the uniqueness of global 
ontology names within any proposed community of usage. Following 
current practice, URI's used as global ontology names are taken to 
refer to a KIF ontology at the location indicated by the URI. [ref: ]

Ontologies can be combined in two ways.

An ontology can include another simply by containing an ontology form 
for the other ontology. In this way one ontology can simply be 
included inside another, and its sentences are considered to be a 
subset of those in the including ontology , and the namespace of the 
included ontology is part of that of the including ontology. In 
effect, the inner ontology form provides a name for a subset of the 
sentences of the larger ontology, simply as a book-keeping 

An ontology can also be imported  by including an expression 
consisting of the word "imports" and the name of the ontology, 
enclosed in parentheses. (The notion of importing is intended to be 
the same as that used in  DAML+OIL [ref: ] .) This allows an 
ontology to include content from ontologies accessed remotely, for 
example from another website, or from elsewhere in an intranet filing 
system. Importation differs from inclusion in that the namespace of 
the importing ontology is disjoint from that of the imported 
ontology. To refer to something with name <name> in <namespace> from 
outside that namespace, one writes <namespace>#<name>. For example, 
if an ontology called 'arithmetic' uses the function name 'plus', 
then the name of this function will be 'arithmetic#plus' elsewhere in 
any ontology which contains the expression '(imports arithmetic)'. In 
this way ontologies may include axioms which use vocabulary 
introduced in other ontologies. (Note. There is one exception to this 
rule, where one ontology consists entirely of declarations and no 
#-prefixing is required. This is used only in sorted KIF.)

As a convenience, an ontology can be given a local name in the 
importing expression, eg
(imports ar
indicates that the ontology at that URL is imported, but that the 
prefix 'ar#' is sufficient to identify words from its namespace. 
Such a local name is considered to be part of the namespace of the 
ontology containing the importing expression. The effect of such an 
importing expression is the same as including the imported ontology 
with every nonlogical symbol #-prefixed by the local name.

Importation is considered to be transitive, and the #-namespace 
convention can be iterated; so for example if the ontology called 
arithmetic at contains an 
importing expression  '(imports it'
and the relation name 'succ' is used in the 'iterations'ontology, 
then this relation may be referred to by the name 'it#succ' in 
arithmetic, and by the name 'ar#it#succ' in any ontology which 
imports it with the local name 'ar', ie which contains the expression
(imports ar

If an ontology at a URL includes another ontology , the included 
ontology can be imported by using the #-prefix to refer to the 
included ontology. For example, if the ontology at includes an ontology form
(ontology sequences ...)
then  the expression
(imports seq
will import just the sentences from the sequences ontology form, with 
the prefix seq# added to all the words in that namespace.

The KIF expression
(imports foo <URI>) ....
corresponds to the following fragment of DAML+OIL:

<rdf:RDF  xmlns:foo="<URI>#" >
<daml:Ontology rdf:about="">
<daml:imports resource="<URI>" />

IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax

This archive was generated by hypermail 2.1.4 : 04/02/02 EST