*** DRAFT *** DO NOT CITE *** LIABLE TO CHANGE WITHOUT NOTICE ***FOR INFORMATION CONTACT Pat Hayes *** FOR BACKGROUND SEE SCL email archive ***
THIS MODEL THEORY HAS SERIOUS BUGS IN THE NOTION OF "FIT".
SEE http://www.ihmc.us/users/phayes/SCL_december_2.html FOR A MORE CORRECT (AND MUCH SIMPLER) VERSION.
Text in this form is comments intended only for the SCL group to read, usually indicating work to be done. @@ indicates something needs to be added or modified.
CHANGE NOTES:
1. redefined 'rigid' This is the likely most general
tractable case, in fact.
2. Redrafted Core skin and use core syntax for examples.
Added scl:Fun back to header vocabulary but with new meaning: Fun(n,R) means
R is functional with n arguments. THis provides a more expressive header vocabulary.
1. Semantics rewritten more coherently, with all 'extras'
included in one table. Also some bugs corrected.
2. Put character strings back into kernel.
2a. Modified kernel to remove name/var distinction (hence no free vars: will
handle this in the core translation)
3. More discursive text, examples, added and reorganized, with discussions
of entailment. **Still incomplete***
4. Function and seqvar fit conditions tightened up and discursive prose written. Explanation
of how to use seqvars for recursion added.
5. Made start on writeup of header absorption, but it would be a lot easier
to do this with the larger core syntax.
***Need to introduce core syntax earlier*** Right after kernel semantics, before
discussion.
1. Lots more text, examples, discussion. Headers, fit and ontology labelling
now seems fairly stable and kernel is OK.
2. Discussion of entailment and quantification over empty function sets.
(??IS this OK? Its got a slight whiff of free logic about it. ** CHRIS, CHECK THIS OUT
AND SEE IF YOU CAN STOMACH IT.**
3. 'core' syntax skin now defined, though syntax BNF needs fixing.
4.
Idea of
a flaying table for defining skins seems to work, but may not be very readable
(??) Next thing to try is doing this for some other forms. KIF next, then
CGs, then RDF/OWL.
5. Core skin handles comment wrappers trivially and also handles the roleset
syntax quite well.
1. section on lexcial flexibility introduces main ideas and justifies them
in terms of interopreability in 'open' context. This actually provides
a nice way of justifying the syntactic freedom.
2. Rewritten mostly the truthrecursion, incorporating the 'fit' notion.
This now handles the full WW syntax (!) but still will allow standard FO
models for GOFOL syntaxes.
3. The kernel is extremely minimal: only single universal quantifiers; put
the definitional stuff back into it so its a complete language.
TO DO.
0. Give some examples and discussion
1. Skindefining framework. (use AS as a general skindescribing technique?
) HARD. must handle sets.
2. provide some standard skins, including core, KIF and CGs. (Z ?)
3. Define comment syntax and alternative atom syntax using roles, as standard
skin techniques.
3a. Maybe give an RDFS skin and an OWL skin as 'Lbase' replacement (?) SLOW
4. Rewrite the definition stuff to take account of headers SLOW
4a. Define header ontology semantics (easy)
4b. Describe headerelimination by guarding quantifiers, apply to FOL
headers
5. provide some standard headers for importing, including lists and FOLstyle
headers. easy
6. Draft XML interchange syntax which does the defining properly, and allows
markup to be mixed with nonSCL text. HARD
7. Describe holds/app embedding for generic SCL. SLOW
8. Handle Tanel's 2equalities issue using 4b+7
9. Fix the bloody syntax.
10. Write up an entire section whcih discusses SCL<>FOL. Putting it all
in one place is good PR.
11. Also write up discussion of importing, labelling, using SCL on a network,
combining ontologies taking definitions into account, etc., Bring out the utility
of the syntactic flexibility. NEED TO THINK ABOUT COMBINING HEADERS. ALSO ABOUT
TREATING SPECIAL NAMES AS DEFINED BY PARTICULAR HEADER THEORIES, LIKE DATATYPE
THEORIES IN LBASE.
Text like this is 'technical notes' which we can use to insert things of interest only to some readers, or asides from the main flow of the text.
0. Introduction
0.1 Discussion and overview
0.2 Surface syntax
0.3 Contextual signatures
1. SCL Kernel
1.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
0.1 Discussion and overview
This whole section probably needs rewriting eventually.
SCL is a firstorder logical language intended for information exchange and transmission. SCL allows for a variety of different syntactic forms, called skins, all expressible within a common XMLbased syntax and all sharing a single semantics. SCL is also selfcontained in the sense that an SCL ontology can express its own signature in SCL.
SCL has some novel features, chief among them being the ability to express the signature of an SCL ontology in the ontology itself, a syntax which allows 'higherorder' constructions such as quantification over classes or relations, and a semantics which allows theories to describe intensional entities such as propositions or properties. Conventional firstorder syntactic forms can be defined in SCL by restricting the signature.
SCL can be embedded within a conventional firstorder logical theory using a commonlyused translation, allowing existing firstorder reasoners to be used as conforming SCL engines with minimal change. Most extant syntactic variants of firstorder logic can be transcribed into an SCL dialect using a generic style of syntactic transformation.
historical notes on KIF and original motivation of knowledge interchange; new role of semantic web.
It is clear that the 'same' logical expression can be rendered in a variety of different syntactic, or even graphical, forms: connectives can be written as infix, postfix or prefix, groupings indicated by brackets, groups of dots or graphically by enclosing circles, etc.. The differences in appearance between surface forms can be quite extreme. A simple logical expression written in introductory textbook form:
(∀x)(Boy(x) → (∃y)(Girl(y) & Kissed(x,y)))
appears in conceptual graph interchange form (CGIF) as:
[@every*x] [If: (Boy ?x) [Then: [*y] (Girl ?y) (Kissed ?x ?y) ]]
and in a KIFlike syntax as:
(forall (?x ?y) (implies (Boy ?x)) (exists (?y) (and (Girl ?y) (Kissed ?x ?y))))
Extremely 'compact' notations have been used, such as the postfix convention which requires no parentheses:
K_{xy}G_{y}&EyB_{x}IAx
while at the other extreme, a hypothetical XML notational style might look like
<formula> <forall> <var>x</var> <formula> <implies> <formula> <atom> <con>Boy</con> <var>x</var> </atom> </formula> <formula> <exists> <var>y</var> <formula> <and> <formula> <atom> <con>Girl</con> <var>x</var> </atom> </formula> <formula> <atom> <con>Kissed</con> <var>x</var> <var>y</var> </atom> </formula> </and> </formula> </exists> </formula> </implies> </forall> </formula>
To provide for information exchange between such a plethora of syntactic alternatives , SCL follows the lead of the KIF initiative by providing a single 'standard' logical language, called the SCL kernel, and a general technique for translating other notations, called SCL skins, into the kernel syntax. Unlike KIF, however, the SCL kernel is extremely small: it is a minimal language sufficient to support the semantics. In order to provide a 'useable' logical language, we define a particular SCL skin called the SCL core which extends the kernel syntax with various logical constructions of proven utility. Throughout the document, the SCL core syntax is used to give illustrative examples.
SCL can be given a variety of skins, and this document defines several which provide SCL variants similar to existing logical notations in widespread use, and an XMLbased syntax, XCL, for general purposes of information exchange. XCL allows documents to 'declare' their skin, or surface syntax form, and can be used as a generalpurpose interchange notation and markup language for any conforming SCL syntax. Finally, a general technique for defining SCL skins in terms of an SCL abstract syntax is described.
In addition to providing for many divergent surface syntactic forms, SCL is designed to allow expressions to be used without making explicit lexical assumptions. Conventionally, a firstorder language is defined relative to a particular signature, which is a lexicon sorted into disjoint sublexica of individual names, relation names and perhaps function names, the latter each associated with a particular arity, i.e. a number of arguments with which it must be provided. This provides a simple contextfree method of checking that all terms and atomic sentences will be wellformed, and allows the usual firstorder semantics to be defined on any wellformed syntax in a contextfree fashion by a simple recursion.
The notion of signature is appropriate for textbook uses of logic. Applied to an interchange situation, however, where sentences are distributed and transmitted over a network (in particular, on the WWWeb) and may be utilized in ways that are remote from their source, this would require that a single global convention for signatures be adopted, which is impractical. SCL therefore is designed to have no builtin assumptions about signatures: it allows information to be combined even when it is written using divergent assumptions about the appropriate signature.
This means for example that SCL must be able to accomodate expressions in which a given term is used both as an individual name and as a relation name, or cases where a relation name is used with different numbers of arguments, or as both a relation and a function name. To this end, SCL is defined with a very accomodating syntax which places minimal restrictions on the lexical roles of names or indeed of terms more generally, and allows relationships between alternatives to be expressed in the language itself.
Such cases arise often in practice. For example, the idea of marriage can be rendered in a formal ontology as a binary relation between persons, or a more complex relation between persons, legal or ecclesiastical authorities and times; or as as a legal state which 'obtains', or as a class or category of 'eventualities', or as a kind of event. Much the same factual information can be expressed with any of these ontological options, but resulting in highly divergent signatures in the resulting formal sentences.
In practice, one can distinguish the intended 'signature role' of any term in a firstorder syntax from its context: if it occurs as the head of an atomic sentence then it must be considered to be a relation; if the head of a functional term with n arguments, then it must be functional on argument sequences of that length; and if it occurs in any argument position then it must be an individual, i.e. must refer to something in the universe of quantification. SCL therefore replaces the idea of a signature with that of occurring in a position as the primary lexical classification for names and terms. This requires a new notion in the metatheory, of an interpretation fitting a set of sentences, in the sense (defined precisely below) that the interpretation assigns appropriate entities to all terms in the expressions according to their positions: terms in relation position must denote relations, in function position must denote functions of the appropriate arity, and in argument position must denote something in the universe of quantification. Interpretations which do not fit a set of expressions are considered to be lexically inappropriate for that set, and play no role in determining semantic properties such as satisfaction or entailment: they are analogous to (and in fact generalize) the notion of an interpretation on a different signature.
SCL provides a generic technique for describing SCL signatures themselves in SCL, by associating a collection of SCL assertions with an SCL ontology in the form of an SCL header. Assertions in the header determine the fit of interpretations of the ontology, rather than the satisfaction conditions: they state the 'syntactic' presuppositions of the ontology, but written in SCL. A special header vocabulary is provided which is sufficient to express all conventional signatures, and various 'standard' headers and header styles are defined. SCL headers are expressed in SCL notation and their interpretation is governed by the SCL semantics, providing a uniform framework for data and metadata. The semantics treats header sentences as though they are asserted in a larger universe of discourse. If the header is omitted or absent, then the generic SCL conventions based on syntactic fit are used.
The lexical flexibility of SCL also covers the case where one sentence treats as an individual something that is considered a relation by another sentence. In fact, SCL does not impose any restriction on the occurrence of terms in other atoms or terms: any term may occur in any position in any atomic sentence or term. This allows quantification over relations and functions, for example, or the use of relationvalued functions, or relations applied to other relations. The resulting syntax is similar to a higherorder syntax; but unlike traditional omegaorder logic, SCL syntax is completely typefree. It requires no allocation of higher types to functionals, and imposes no type discipline. Selfapplication is not prohibited, for example. All of the following are legal SCL syntactic forms for an atomic sentence:
R(a b)
x(R b)
R(a)(b c)
R(a(b(R)))
x(x(a) x)
R(R)
The third example has R
denoting a function with a binary relation
as a value; the fourth example has R
denoting a relation which
is also an individual, and to which the function b applies. To satisfy the
last example, the variable x
must denote
something playing all three syntactic roles: a functional binary relation which
is also in the universe of discourse and which holds of one of its functional
values and itself.
An atomic sentence may be written with no arguments:
R()
and then must denote an entity with a truthvalue, i.e. a proposition.
Note the distinction between R()
and R
:
the former denotes a truthvalue; the latter, a relation. Similarly x()
can
be used to play the role of a propositional variable. The lack of any comprehension
principle in the SCL semantics means, however, that it is not valid to substitute
arbitrary propositional sentences for such a variable.
As has been previously noted on several occasions [ref HILOG][refHenkin?], a superficially 'higherorder' syntax can be given a completely firstorder semantics simply by refusing to countenance any logical comprehension principles, and allowing the universe of relations to be of arbitrary size. SCL is semantically firstorder in this sense, and satisfies all the usual semantic criteria for a firstorder language, such as compactness and the SkolemLowenheim property. SCL syntax can be uniformly translated into a conventional firstorder theory using a conventional syntax defined by a simple signature. This 'holdsapp' translation is familiar and widely used in ontology applications, but is described in detail in section @@ below for reference purposes; as described there, some care is needed when treating equality.
SCL treats functions as a special class of relations. A relation is (n)functional
, or simply a function, when it holds of a single, unique first
argument for each sequence (of length n) of the remaining arguments. The SCL
convention is that the first argument is the value
of the function applied to the remaining arguments; thus, if R
is
a relation symbol denoting a 2functional relation then the atom R(a
b c)
is
equivalent to the equation a =
R(b c)
.
This differs from the convention used in Prolog [refProlog]
where the function value is written as the last argument of a relation.
The present convention was chosen to better integrate with the use of sequence
variables. Note that the arity of the function is the
number of relational arguments, so is one more than the number of
functional arguments: in this case the arity of R
is 3.
In SCL, simply using
a term in a functional position implicitly asserts that it denotes a function,
since any interpretation in which it does not fails to fit the syntax of the
expression. Thus the bare assertion of the equation a = R(b c)
actually
says rather more than the corresponding relational form R(a b c)
,
since
the latter is satisfied by interpretations where R
is not functional.
The presence of functions in the syntax complicates the definition of 'fit' somewhat. In order to ensure that every term has a welldefined denotation, the semantic recursion must ensure that any term in function position must denote a relation which is functional for the appropriate length argument sequence. In order to
Finite sequences play a central role in SCL syntax and semantics. All atomic sentences (and complex terms) consist of an application of one term, denoting a relation, to a finite sequence of other terms. Such argument sequences may be empty, but they must be present in the syntax, as an application of a relation term to an empty sequence does not have the same meaning as the relation term alone.
SCL also allows relations (and hence functions) to be used applied to any number of arguments: such a relation is called variadic. For example, This would allow for example Married to be be used as a binary relation name, a unary property name, and a fourplace relation between persons, marrying authorities and timeperiods, without needing to use three different formal names for the same concept.>
SCL follows KIF also in providing a special syntactic form called sequence variables to allow generic assertions to be made which apply to arbitrary argument sequences. An SCL axiom using sequence variables can be viewed as a firstorder axiom scheme, standing in for a countably infinite set of firstorder instances.
Sequence variables are restricted in SCL to occur only in the last position in an argument sequence, and are not bound by quantifiers: this keeps the language firstorder and makes unification tractable. Sequence variables can be replaced by a more conventional notation, at some considerable cost in elegance, by introducing argument lists to the ontology explicitly: we provide a generic header which can be used for this kind of elimination, which is commonly adopted in practical KR notations.
If an argument sequence ends with a sequence variable, then the presence of the variable indicates that the sequence may be arbitrarily extended, and is required to hold for all the possible extensions.
Sequence variables are quite a powerful device: in effect, they allow a finite sentence to assert infinitely many quantifications all at the same time. Indeed, if arbitrary quantification over sequence variables is permitted, then the resulting language is a subset of the infinitary logic L_{w1w}, of a higher expressiveness than firstorder logic, and for example is not compact [refHayMenzel]. The restrictions on sequence variables in SCL have been chosen to restrict the language to firstorder while providing much of the practical utility of sequence variables for writing 'recursive' axioms to define lists and other recursively defined constructions.
The SCL kernel is the minimal logical core of SCL. All other extensions and alternative forms for SCL can be defined in terms of constructions expressible in the kernel, which thus provides a fixed reference for the ultimate expressiveness of any SCL expression in any SCL syntactic form.
The kernel syntax is designed to be as simple as possible and is not recommended for either readability or for use as an interchange or markup notation. The SCL core syntax and XCL, respectively, are more suitable syntactic forms.
As noted above, the kernel is unusual in the relatively free licence it gives to the syntactic structure of atomic sentences. This freedom slightly complicates the model theory, but allows for a uniform treatment of a larger variety of notational conventions within a single framework. Conventional firstorder syntax is a special case where sequence variables are omitted and the lexical space of names can be sorted into distinct relational, functional and individual names in a contextfree manner.
An SCL ontology, or simply an ontology, is any set or sequence of SCL sentences together with an optional header, which is itself a set or sequence of SCL sentences.
The kernel syntax uses sequences throughout, for convenience in defining iterative syntactic operations, but no particular significance attaches to the ordering of the sequence, and other SCL skins may adopt a setbased syntactic convention.
Headers have a special semantic role: they provide a general method for encoding syntactic and other 'background' information about the ontology. They are treated in a distinct way in the kernel semantics. The kernel also provides a toplevel ontology definition syntax which associates a name with an ontology, and a importing syntax, which indicates that a named ontology is being included into an ontology.
The choice of the term "ontology" is not intended to convey any particular category or to indicate an intended use, but is simply a neutral terminology used to refer to a coherent piece of SCL which can be published, transmitted or asserted as a coherent single document: the topmost level of the syntax. Other synonyms in widespread use in various communities include "knowledge base", "axiom set" , "set of sentences", "metadata", "data model" and "model", as well as such particular usages as "RDF graph" and "document".
A kernel sentence is either quantified, or boolean, or atomic. In order to keep the SCL kernel small, only universal quantification, negation and conjunction are assumed, and no explicit syntactic markers are provided for conjunction or quantification: a conjunction is simply a sequence of sentences, and the quantifier is indicated by the binder. (The SCL core skin supplies a fuller, more conventional, logical notation, described in section @@ below.)
Atomic sentences, or atoms, are formed from terms (denoting relations) and sequences of argument terms (denoting entities in the universe of discourse between which the relation holds), and an optional sequence variable which if present indicates an arbitrary extension to the argument sequence.
The order of terms in an argument sequence is semantically significant. The SCL Core skin defined in @@ provides for an alternative unordered syntax for argument sequences, based on role sets.
Terms are either lexically primitive names, or are themselves formed in a similar way to atoms (in fact, the SCL kernel syntax for terms and atoms is identical: they can be distinguished only by context). As discussed above, SCL allows a typefree syntax where the relation of an atom or the function of a term may be indicated by a general term, including a variable.
The SCL kernel includes several special names, which are required to satisfy special semantic conditions. These include decimal numerals and quoted character strings, and a special header vocabulary used to express syntactic constraints inside headers. Other SCL skins may describe further categories of special name in addition to the kernel categories.
The kernel syntax and semantics
both use sequences in several places. A sequence (tuple, vector) over
a set S is a totally ordered finite subset of S, written <s1,...,sn>;
n is the length of the sequence. The notation <s1, ..., sn;
<t1,...,tm>> indicates
the concatenated sequence <s1, ..., sn, t1,..., tm>. The unique empty
sequence is written <> and has length zero.
In the kernel syntax, a sequence
of sentences (enclosed in parentheses) is considered to be a sentence whose
meaning is the conjunction of the sentences in the sequence. The empty sequence
of sentences, indicated by an empty parenthesis pair '( )
',
therefore can be treated as the truthvalue true.
As noted earlier, SCL treats functions as a special class of functional relations. A set of finite sequences over U is nary functional,or functional at n, when for every sequence <x1,..., xn> of n elements of U, the set contains exactly one sequence <y, x1,...,xn>, and partially functional at n when it contains at most one such sequence. It is (partially) functional above n when it is (partially) functional at every m greater than n, and is (partially) functional when it is (partially) functional at n for every n.
Note. This includes the case n=0, so a partially functional set can contain at most one singleton sequence, and cannot contain the null sequence. The first item in a sequence in a functional set is conventionally regarded as the value of the function applied to the remaining items. As noted, this differs from the convention used in Prolog [refProlog] where the function value is written as the last argument of a relation.
Note. The empty set is partially functional.
The formal syntax of the kernel is g
SCL kernel syntax, part 1, logical grammar 
ontologyDefinition = ( ontology plainname
= ontology ) 
SCL kernel syntax: part 2, lexical grammar
Note, this EBNF doesnt deal with whitespace. This will need to be fixed. 
seqVar = @character* 
The special sentence form using imports is permitted only at the top level of an ontology: it is used to include one ontology into another.
The SCL kernel distinguishes numerals as a special class of names. Any numeral used in any expression is required to denote an integer in the conventional decimal way. It also allows quoted strings to be used as names; they refer to the enclosed character string (with occurences of any backslash character immediately preceding a single quote or another backslash removed).
The SCL semantics is sensitive to the way that terms are used, since their syntactic location imposes different requirements on what they are required to denote. This is made precise by the notion of position, which is defined in terms of the sytanx of terms and atomic expressions. Any term which occurs as the first item in an atomic sentence is said to occur in relation position; the first term in any other term occurs in function position, and any term occurring in any other position in any atom or term is in object position. Note that a single name may occur in more than one type of position in a sentence or ontology, and that if a name occurs in a position in any expression then it also occurs in that position in any larger expression or set of expressions. The occurrence of a term in a position in an expression constrains the possible interpretations of the expression, as explained below.
Position also determines variablehood. A name occurring inside the initial parentheses of a quantifier is considered to be a variable: all occurrences of that name in the body of the expression are bound by that quantifier; other names are free.
Several special cases of the kernel syntax can be identified, largely by restrictions on the syntax of atomic sentences and terms.
An ontology is firstorder if it contains no sequence variables, the only terms which occur in relation or function positions are constants, and every constant occurs in only one kind of position. This corresponds to the traditional notion of a firstorder signature: the names in the vocabulary can be subdivided into relation, function and individual names, each occurring only in its alloted role in the syntax.
If no term occurs in function or relation position in two atoms or terms with different numbers of arguments, then the ontology is fixedarity.
If no variable occurs in any term in function position, then the ontology is rigid. Rigid ontologies represent a useful compromise between the syntactic freedom of general SCL and the syntactic predictability of a conventional firstorder syntax, as the fitting conditions on an interpretation are much easier to state and to check when quantifiers cannot bind function names. Notice that rigidity only restricts the occurrence of variables inside terms in function position: a rigid ontology allows arbitrary terms to occur in relation position, and names in relation position may be bound by quantifiers.
If all terms are names, so there are no expressions in function position, the ontology is pure relational.
The SCL kernel syntax is a minimal logical syntax, and requires that expressions be transformed in ways that are not always intuitive to read. For example, the sentence 'every boy kissed a girl' appears thus in the kernel syntax, which has no syntactic primitives for implication or existential quantification:
(x)
not ( Boy(x) (y) not ( Kissed(x y) Girl(y) ) )
We can define a more readable notation in the form of a skin. An SCL skin is a formal language together with a uniform translation of some of its grammatical categories into SCL kernel expressions, so that the meaning of those expressions is given by the translation. By convention, any expressions in any SCL skin which are not translated into SCL content are ignored by SCL; in effect, they are treated as transparent comments as far as the SCL is concerned. This allows an SCL skin syntax to used inside other textual material without causing any interference with the SCL content being expressed. We will describe skins using EBNF with certain grammatical categories indicated as SCL contentful, and giving a translation table for expressions of these categories into the SCL kernel.
Note, this syntaxmapping business is done rather informally and in an adhoc fashion. Future drafts will provide a more precise technique for defining alternative syntax skins, maybe using an existing system of syntaxdescribing conventions if a suitable one can be found. We are currently investigating MOF. The current treatment should be considered a temporary measure.
The following tables define a simple SCL skin called the SCL core which we will use for giving examples throughout this document. Other skins are defined in later sections.The SCL core syntax extends the kernel syntax using the same general style for atomic sentences but providing explicit names for the quantifiers and connectives, adding other conventional logical notation and a variety of useful conventions, including guarded quantifiers and 'argument roles'. The Core uses almost the same lexical syntax as the kernel, with one change (indicated in red) to allow variables to be syntactically distinguished.
SCL Core syntax: lexical grammar
Note, this EBNF doesnt deal with whitespace. This will need to be fixed. 
variable = ?character* 
SCL Core syntax, logical grammar 
ontologyDefinition = ( scl:ontology plainname = ontology ) 
A variable occurring in a boundvarSeq is bound in the quantified expression, otherwise it is free.
The semantics of the SCL Core are established by giving a systematic translation from any Core expression to an equivalent SCL kernel expression representing its intended meaning. Such a translation of an SCL skin syntax is called a skinning, and is described here using a skinning table. This uses the following conventions.
Symbols in boldface indicate syntax, other symbols are metavaraibles indicating syntactic parts of an expression. Sequences of expressions are indicated using a conventional threedots notation. The skinning of an expression or part of an expression E is indicated by [E].
An expression new means a plainname lexical item which is not used elsewhere in the translation and is different from any other lexical item occurring in the expression.
E[s/t] is the expression E with t substituted for every free occurrence of s.
The entry transparent means that the same syntactic form is used in both the skin and the kernel, and so the skinning process should be understood as applying to every subexpression of the expression. The transparency of the category name depends on the fact that every Core name is also a legal kernel name, and also shows that the Core uses the same special names.
In some cases, the skinning recursion goes 'through' expressions which are not legal SCL core syntax. This technique is used for example to ensure that the same new variable is used throughout the translation of a roleset atom, and to ensure that the deMorgan translation of a disjunction is carried out properly.
Core expression E of category  with syntactic form  translates to kernel expression [E] 
ontologyDefinition  transparent  
ontology  transparent  
topsentence  s with a free variable v  (new)[s[v/new]] 
s with no free variables  [s]  
quantifiedsentence  forall (v...) s  (v) [ forall (...) s] 
forall (v::n ...) s  (v) not (n(v) not [forall (...) s] )  
forall ( ) s  [s]  
exists (v...) s  not (v) not [exists (...) s]  
exists (v::n ...) s  not (v) not (n(v) [exists (...) s])  
exists ( ) s  [s]  
conjunction  s & ...  ([s] [& ...] 
& s & ...  [s] [& ...]  
& s  [s])  
disjunction  s or ...  not ( not [s] [or ...] 
or s or ...  not[s] [or ...]  
or s  not[s])  
implication  s implies t  not ([s] not [t]) 
bicond  s iff t  (not (([s] not [t]) not ([t] not [s])) 
negation  not s  transparent 
atom  r(t1 ... tn)  transparent 
r(t1 ... tn @s)  
r{n=t ...}  not (new) not ( r(new) n([t] new) [{...},new]  
{n=t ...}, v  n([t],v) [{...},v]  
{},v  )  
true  ( )  
( s )  [s]  
term  transparent  
name  transparent 
Most of this is a standard translation of conventional logical notation into the andnotforall fragment represented by the kernel. The core syntax allows the use of restricted quantifiers, with the usual meaning, and allows quantified variables to be grouped together. It also provides a 'roleset' syntax for atoms as an alternative to the argumentsequence syntax. Atomic sentences of the form
Married{wife=Jill husband=Jack}
are considered to take a set of arguments in the form of rolevalue pairs. (The skinning table assumes that this set has been ordered in some arbitrary way.) In this roleset syntax, the connection between the relation and its arguments is indicated by the role labels rather than by position in an argument sequence, which avoids the necessity of remembering the argument order when writing sentences, and provides some insurance against errors arising from sentences using different argumentorder conventions.
In SCL Core, the roles are considered to be binary relations between an entity to which the main predicate applies and the argument, so for example the above atom is equivalent to the existential conjunction:
exists (?x) Married(?x) and husband(Jack ?x) and wife(Jill ?x)
where ?x
indicates an entity which has been variously called
an eventuality, fact, situation, event, state or trope,
and might be rendered in English as "Jack and Jill's being married" or "the
marriage of Jack and Jill".
For SCL purposes however it is possible to think of ?x
more prosaically
as being an argument sequence, and the rolenames as selectors on the elements
of this sequence. Under the presumption that rolevalues are unique, the above
can be written using equality:
exists (?x) Married(?x) and Jack=husband(?x) and Jill=wife(?x)
which illustrates the intuitive interpretation of role names as argumentsequence selection functions.
This syntax allows arguments to be provided in a piecemeal
fashion, and allows arguments to be omitted: such arguments are implicitly
existentially quantified. In fact, any such atom entails a similar atom with
some rolepairs omitted. Notice the difference in meaning between R(
)
and R{ }
. The former asserts positively that R
is
true of the empty sequence, while the latter merely asserts that R
is
true of something, to which other things may be related by unknown roles; for
example, Married{}
asserts simply that a marriage exists.
This roleset convention does not of itself specify any relationship between the same fact expressed as an argument set and using an argument sequence: but since SCL allows variadic relations, it is possible to use the same relation in both ways; and they can be related axiomatically by for example writing
(Married(?x ?y) and Married(?z) ) implies ( ?x=wife(?z) and ?y=husband(?z)
)
which indicates the convention by which a wife must be the first argument of a marriage.
Comment that purpose of this is not to actually do the
translation at runtime, but rather to define it exactly so that semantics of
the core is defined by the MT of the kernel. Remark that flaying can be done
in stages so that eg other syntaxes can be reduced to core, providing a larger
'base' of expressions to translate into.
Maybe give MT for core in an appendix? Later, later.
The skinning table can be written perhaps more intuitively by using the core syntax itself in the third column, rather than translating directly into the kernel syntax. Taking advantage of this provides the following table, whcih can of course be used to derive the earlier one:
Core expression E of category  with syntactic form  translates to kernel expression [E] 
ontologyDefinition  transparent  
ontology  transparent  
topsentence  s with a free variable v  (new)[s[v/new]] 
s with no free variables  [s]  
quantifiedsentence  forall (v...) s  (v) [ forall (...) s] 
forall (v::n ...) s  [ (forall (v) n(v) implies s )]  
forall ( ) s  [s]  
exists (v...) s  not (v) not [exists (...) s]  
exists (v::n ...) s  [ (exists (v) n(v) & s )]  
exists ( ) s  [s]  
conjunction  s & ...  ([s] [& ...] 
& s & ...  [s] [& ...]  
& s  [s])  
disjunction  s or ...  not ( not [s] [or ...] 
or s or ...  not[s] [or ...]  
or s  not[s])  
implication  s implies t  not ([s] not [t]) 
bicond  s iff t  [ (s implies t ) & (t implies s) ] 
negation  not s  transparent 
atom  r(t1 ... tn)  transparent 
r(t1 ... tn @s)  
r{n=t ...}  [ exists (new) ( r(new) & n([t] new) & [{...}, new] ]  
{n=t ...}, v  n([t],v) & [{...},v]  
{},v  )  
true  ( )  
( s )  [s]  
term  transparent  
name  transparent 
The semantics of the SCL kernel is defined in terms of a relationship of satisfaction between SCL ontologies and interpretations, in the conventional way. However, the need to provide for a generic contextual signaturefitting mechanism requires that we define two notions in parallel: that of an interpretation fitting an expression, and the conventional notion of a value of an expression in any interpretation which fits the expression. Interpretations which do not fit an expression are not required to assign a value to that expression. Interpretations are defined relative to sets of names, called vocabularies. The set of names which occur in an ontology O will be called the vocabulary of O.
An SCL interpretation of a vocabulary consists of two sets and two mappings:
SCL interpretation I of a vocabulary V 
a nonempty set U_{I} called the universe, members of which are called individuals of I; a set R_{I} , members of which are called the relations of I; a mapping ext_{I} from R_{I} to sets of finite sequences of elements of U_{I} , called the extension mapping; a mapping int _{I} from V to (U_{I} union R_{I} ),
called the
interpretation mapping. 
We may omit the subscripts when no confusion would arise.
No conditions are placed on the relationship between U and R; in particular, they may be disjoint, or R may be fully contained in U. The extension mapping is a formal device to distinguish a relation considered as an object from its extension, which permits an intensional view of relations and allows relations to be applied to other relations, and even to themselves, without violating the axiom of foundation. If I(name) is in R, then ext(I(name)) is the conventional firstorder interpretation of the relation name: a conventional firstorder interpretation structure can thus be obtained as a special case of an SCL interpretation where ext is the identity. A relational extension may contain sequences of any length, in order to allow for variadic relations.
A mapping on a set S of names and/or seqVars is a function from names in S to (U_{I} union R_{I} ) and from seqVars in S to sequences over (U_{I} union R_{I} ); we will use A, B, etc. to indicate mappings. If I is an interpretation then IA is the interpretation which maps elements in the domain of A using A, but is otherwise like I. This notation associates to the left, so that int_{IAB}(x) = int_{(IA)B} = B(x) when x is in the domain of B.
This convention ensures that names are bound by their innermost containing quantifier.
The semantic conditions for ontologies with headers requires an auxiliary definition. Say that an interpretation I is a shrinking of J, and that J is an expansion of I, when I can be obtained from J by deleting some things from the universe of I. Formally, when: U_{I} is a subset of U_{J}, R_{I} is a subset of R_{J}, and for all x in R_{I}, ext_{J}(x) = ext_{I}(x). The expansion J may include some entirely new relations, but it cannot change the extensions of relations named in I.
Finally, the idea of naming an ontology makes sense only if we can assume some 'global' naming convention which has a larger scope than a single ontology, and which interpretations are required to respect. In XCL we will use URI references as global names. in accordance with the emerging WWWeb conventions. For now, we simply assume that there is a fixed function ont from ontology names to ontology values. The exact nature of ontology values is not specified, other than that they are entities which can be parsed into SCL kernel syntax and to which an interpretation mapping can be applied. (One can think of an ontology value as a quoted string containing a character representation of an ontology written using the kernel syntax.)
SCL interpretation I of an expression E  
if E is a  of the form  then I fits E if  and I(E) = 
plainname  n  int_{I}(n) is in U_{I}  int_{I}(n) 
specialName  
numeral 
the decimal value of numeral  
'string' 
string with occurrences of \ preceding \ or ' deleted  
scl:Integer 
ext_{I}(I(E)) = {<n>: n an nonnegative integer }  
scl:String 
ext_{I}(I(E)) = {<u>: u a Unicode character string }  
scl:Ind 
ext_{I}(I(E)) = {<x1,...,xn> : x1,...,xn all in U_{I} }  
scl:Rel 
ext_{I}(I(E)) = {<x1, ..., xn>: x1,..., xn all in R_{I} }  
scl:Fun 
ext_{I}(I(E)) = {<m, x1, ..., xn>: x1,...,xn all in R_{I} and ext_{I}(x1),...,ext_{I}(xn) all functional on m  
scl:Arity 
ext_{I}(I(E)) = {<m, x1, ..., xn >: x1,...,xn all in R_{I} and ext_{I}(x1),...,ext_{I}(xn) all contain an s with length(s)=m  
term sequence  (t1 ... tn) 
I(t1) is in U_{I}; ... I(tn) is in U_{I}  <I(t1),..., I(tn)> 
(t1 ... tn @v) 
I(t1) is in U_{I}; ... I(tn) is in U_{I}; 
<I(t1),..., I(tn) ; I(@ v)> 

term  f seq 
if t in 
x, where ext_{I}(I(f )) contains <x
; I(seq )> 
atom  r seq 
if t in 
true if ext_{I}(I(r )) contains I(seq ),
otherwise false 
(t1 = t2) 
I(t1) is in U_{I }I(t2) is in U_{I} 
true if I(t1) = I(t2), otherwise false  
booleanSentence  (not s) 
I fits s  true if I(s) = false, otherwise false 
(s1 ... sn) 
I fits all of s1,..., sn  true if I(si) = true for all i, 1<= i <= n, otherwise false  
quantifiedSentence  (var) body 
I fits body 
if for every B on {var }such that IB fits body , IB(body )
= true, then true; otherwise, false. 
topsentence  (scl:import name) 
I fits ont(name)  false if I(ont(name)) = false, otherwise true 
sent 
I fits sent  if for every A on the seqVars in sent, IA(sent)
= true, then true; 

ontology  (head :: body) 
I fits body and for some expansion J of I, J(head)=true  I(body) 
ontology definition  (scl:ontology name = body) 
I fits body  for any interpretation J, J fits ont(name) iff J fits body; and J(ont(name)) = true iff J(body) = true. 
The truthcondition for imports are stated 'backwards' in order to ensure that an importing of an 'impossible' ontology is vacuous, and does not produce a contradiction. This is a technical convenience.Note that since the toplevel truthconditions override any assignments to free variables and seqvars in a sentence, the vocabulary of an ontology can be restricted to the constants and special names which occur in the ontology (and any imported ontologies) without loss of generality.
The reason for requiring that an expansion of I satisfies the head of an ontology, rather than I itself, is because in general the header may use relations which are not in the intended signature of the body, and may need to quantify over entities, such as relations of the ontology, that are not in the intended universe of discourse. This is discussed further below, and a general technique is given for mapping any such ontology into a 'plain' ontology with an empty header.
I is an interpretation of E when I is an interpretation on the vocabulary of E and I fits E; and I satisfies E when it is an interpretation of E and I(E)=true.
The notion of 'fitting' used here corresponds to the fact that the exact grammatical role of a name can only be determined from the context of its use in a larger SCL expression, as discussed earlier. As described below, ontology headers can be used to partition the lexical space of names of the ontology body so that all grammatical role(s) can be determined from the name in a contextfree manner. In such cases the interpretation conditions can be applied directly to the vocabulary, and the ontology fit is automatic. However, more flexible 'syntactic' usages are also possible.
An ontology definition is required to have miraculous powers: if it is ever true in any interpretation, then the name is attached to the defined ontology in all interpretations. Thus, if by convention we say that publishing any SCL amounts to asserting it, then asserting an ontology definition requires any interpretation of any SCL ontology containing an importation of that name, to treat it as having the same effect, both upon the fit and upon the truthvalues, as copying out the sentences of the defined ontology in place of the importation. To actually achieve such miraculous powers requires a global naming convention: XCL uses universal resource identifiers [refRFC2396] for this purpose.
The four relation names scl:Ind
, scl:Rel
, scl:Fun
and scl:Arity
are called the header vocabulary. The header vocabulary can
be used anywhere in any SCL ontology; but when used in an ontology header,
the semantic conditions require that the header classifications are understood
to refer to interpretations of the body of the ontology, rather than of the
header itself. To see the difference this makes, consider the following ontology
with an empty header:
(( ) ::
( not scl:Ind(R) ))
.
This is a contradiction  has no satisfying interpretations
 since any interpretation which fits the inner sentence would require R
to
denote an individual in U, but the sentence asserts that is not in U.
The sentence
forall (?x)scl:Ind(?x)
is
a tautology in any ontology body, since scl:Ind
is true of everything
in the universe: one could in fact transcribe scl:Ind(term)
in
the body (though not in the header) as any tautologous assertion, in particular
as ( term
= term
).
However, the same sentence in the header yields a satisfiable ontology:
((
not scl:Ind(R) ) :: ( R(a) ))
This is satisfied for example by an
Herbrand interpretation H in which the interpretation mapping is the identity,
with U_{H}={a
}, R_{H}={R
} and ext_{H}(R
)={<a
>};
the fit is guaranteed by the extension J with U_{J}={a
, R
},
R_{J}={R
, scl:Ind
} and ext_{J}(scl:Ind
)={<R
>}.
Note that although R
is an individual in J, it is not in H;
and that the interpretation rules
for the entire ontology require that ext_{H}(scl:Ind
)
= {<a>}.
If the body of the ontology had 'misused' the relation symbol as an individual name, for example:
(( not scl:Ind(R) ) :: ( Q(R)
))
then once again the ontology would be unsatisfiable, since there are no interpretations which fit such an ontology, so no interpretations which satisfy it. However, it is useful to distinguish this kind of unsatisfiability from an unsatisfiability arising from a simple contradiction in the body of the ontology, such as:
(( ) :: ( Q(R) not Q(R) ))
since in the former case the body alone is satisfiable. The contradiction in the first case arises from an essentially syntactic incompatibility between the fitting conditions proscribed by the header, and the actual usage in the body.
We will describe this case, of an ontology which has no interpretations which fit it, as an unfit ontology. Unfit ontologies have no interpretations, so have no satisfying interpretations; but their unsatisfiability arises from a different source than a mere contradiction. SCL applications may consider an unfit ontology to be a syntactic error, even if the unfitness can only be detected by semantic reasoning processes.
The header vocabulary
can be used in fairly obvious ways to 'declare' constraints on
the allowable signature of an ontology. A conventional firstorder language
can be specified by asserting scl:Ind
of
every individual constant name and scl:Rel
of
every relation (or function) name, and specifying the arity of
each relation and function using scl:Arity
.
For example the following header specifies a small conventional
firstorder language signature suitable for expressing the earlier
example:
(
forall (x) not( scl:Ind(x) and scl:Rel(x) )
scl:Rel(Boy Girl Kissed)
1 = scl:Arity(Boy)
1 = scl:Arity(Girl)
2 = scl:Arity(Kissed)
)
The first sentence expresses the conventional that relation symbols must not be used as individual names and vice versa: this is satisfied by every conventional firstorder signature. The arity assertions here take advantage of the SCL fitting conditions. Note that it is consistent to allow a relation to take several different numbers of arguments, in general, so for example this is consistent:
scl:Arity(2,R)
and scl:Arity(3,R) and scl:Arity(5,R)
but the use of 'scl:Arity
' in
a function position requires that it denote a functional
relation in any fitting interpretation; so the only consistent
way to interpret this header is with scl:Arity
interpreted
as a functional relation, ensuring that all relations in the
body have a fixed number of arguments.
An ontology with an empty header will be called a plain ontology. Since an empty sequence is trivially true, the fitting conditions on an empty header are vacuous, so plain ontologies determine the fit of an interpretation solely by the way that terms occur in their atomic sentences. All SCL ontologies can be mapped into a plain ontology, which therefore provide a kind of universal common form for SCL ontology manipulation by inference engines.
An ontology definition assigns a name to the ontology which all other ontologies
are required to recognize when it is used in a import assertion in the top
level. The effect of including an importation is similar to writing
out the sentences of the named ontology in place of the scl:import
sentence;
however, there is no requirement that this process of copying actually be performed.
If the named ontology is plain, importation is exactly like copying. If the named ontology has a nontrivial header, the semantic and fitting conditions inherited from the header are required to apply in the importing ontology. For example:
( scl:ontology http://purl.org/scl/1.0/#ex1= (( 1
= scl:Arity(Boy) )::( Boy(Jack) )) )
(( ):: ( (import http://purl.org/scl/1.0/#ex1) Boy(a b) ))
The second ontology is unfit, even though it has an empty header, since Boy
is
required by the imported header to have arity exactly 1, but is used here with
arity 2. In effect,
A header can itself be considered to be an ontology, so can be given a name:
(scl:ontology http://purl.org/scl/1.0/#exJ&J
= (()::( (?x)not ( scl:Ind(?x) scl:Rel(?x) ) scl:Ind(Jack
Jill) scl:Rel(Boy Girl Kissed) (1 = scl:Arity(Boy)) (1 = scl:Arity(Girl))
(2 = scl:Arity(Kissed)) ) )
and then when imported into a header has the same effect as writing out the above sentences into the header:
((
(scl:import http://purl.org/scl/1.0/#J&J ) :: ( ...
))
This provides a useful general technique for rapidly assembling suitable headers from a stock of standard headers. Several 'standard' header ontologies are defined in section @@ below, and users are encouraged to invent and publish others. One such standard is the SCL header header, which can be used as a header for most SCL headers, if required for purposes of syntax checking:
(scl:ontology http://purl.org/scl/1.0/#HeadHead = (()::(
scl:Integer(?x)
implies scl:Arity(?x scl:Ind scl:Rel scl:Fun scl:Arity)
scl:Fun(?x @r) implies scl:Arity(?x @r)
scl:Fun(?x @r) implies scl:Rel(@r)
scl:Arity(1 scl:Integer)
scl:Arity(1 scl:String)
)
The truth of a quantified statement depends only on the instances which fit the body of the expression. When the variable occurs in a function position (or, more generally, inside a term used which occurs in function position) the requirements of 'fitting' can be quite strict, and hence severely limit the range of the quantifier, even making it empty. This situation can easily arise when the term also contains a sequence variable. This can be illustrated by the following example:
R( R(@x) @x)
This seems to assert that R
is a functional relation, since @x can be bound
to a sequence of any length. And indeed it does assert this: but it does so
trivially, simply by virtue of the use of R
in the function position in the
inner term. The fitting conditions alone require that R
be functional.
To see this, suppose that I
satisfies the expression; then for any map A from @x
to
a sequence <x1,...xn>, int_{I}(R
) must be in R_{I} (or
else I does not fit the expression) and ext _{I}(I(R
))
must be functional on n (or else IA does not fit the expression). But this
must apply for any n: so I(R
) is functional.
The same effect can be achieved by making an apparently tautologous assertion using this term, such as
R(@x)=R(@x)
This also asserts that R
is functional. Simply writing the term itself implicitly
asserts this, regardless of the surrounding context, since only interpretations
in which it is functional will fit the syntax of the expression.
The exact form of the constraint can be read off the term syntax in an obvious
way: the term R(a b @x)
requires that R
is functional
above 2;
R(a)=R(a)
asserts that R
is functional at 1,
and so on.
This means in turn that the corresponding universal generalization is true in all SCL interpretations:
?f( ?f(@x) @x)
It would be easy to read this example intuitively as making the very strong claim that all relations in the universe were functional, since it seems to quantify over a variable in relation position. However, that reading would be mistaken. The key observation is that the variable also occurs in function position, so is required to range only over relations which are functional in the required way: in this case, by virtue of the sequence variable, relations which are functional on n for all n. Simply using a name in a function position requires that it denote a relation which is functional in whatever way is required by the rest of the expression, and so in effect restricts the scope of the enclosing quantifier to appropriately functional relations rather than all relations.
The full argument is as follows. Suppose I is any satisfying
interpretation and A maps @x
to
a sequence <x1,...xn> , and B maps f
into (U
union R),
and consider IAB('(f
(f @x) @x)
'). If
B(f
) is not in R then IAB does not fit the atomic
syntax (f ... @x)
; if B(f
) is not functional on
n then IAB does not fit the term syntax (f @x)
; if B(f
)
is in R and is functional on n then there is a unique x with <x,x1,...,
xn> in ext(IAB(f
)) = ext(B(f
)) , and then the
truthconditions on terms and atoms conspire to ensure that the expression
evaluates to true. So for any such mapping B, either IAB does not fit the syntax,
or IAB('(f
(f @x) @x)
')=true; so IA('(f) (f (f @x) @x)
')=true; and
this is so for any mapping A on '@x
'; so I('(f) (f (f @x)
@x)
')
= true.
As this example suggests, universal quantification over names in function position can have a smaller scope than one might expect. It is important to bear this in mind when interpreting SCL quantifiers which bind function names. Simply using a name in a function position requires that it denote a relation which is functional in whatever way is required by the rest of the expression, and so in effect restricts the scope of the enclosing quantifier to appropriately functional relations, rather than all relations. The fitting conditions on terms in relational position are much less restrictive: only the function position places any constraints on the extension mapping used by an interpretation, for example.
The SCL universe is required to be nonempty, but there is no requirement that an interpretation provide any functional relations, so the 'universe' of functions may be empty. This means that while SCL syntax allows quantification over functions, such a quantification may be a universal assertion about an empty set, and hence vacuously true. This means that a universal sentence in which the bound variable occurs in a function position, such as:
forall (?f) S(?f(a) b)
does not entail the corresponding
existential assertion: exists (?f) S(?f(a) b)
For example, the Herbrand interpretation I with U_{I}={a,b}, R_{I}={S}
and ext(S)={<a a >}satisfies the former vacuously, by virtue
of there being no functional relations in the universe to which f
can
be mapped; but I does not satisfy the second sentence.
Note however that the universal sentence does entail any instance of itself, since the introduction of the term used to do the instantiation is itself enough to ensure that any fitting interpretation will contain a relation of the required functionality. In order to be able to support the instantiation, the language must be sufficiently enriched so as to ensure that the quantifier is no longer vacuous. The failure of the universal sentence to entail its existential equivalent in a case like this can be seen as an artifact of the extreme lexical poverty of the language. For example, it would be possible to insist that the universe contains a sufficient 'stock' of
Since the property of being functional can itself be stated in SCL, it is possible for an ontology to be inconsistent by denying its own fitting conditions, for example
R(a c) and R(b c) and not a = b and d = R(e)
is inconsistent,
since R
must be functional in order to fit the last sentence,
but is asserted not to be by the first three sentences.
All of these rather arcane issues only arise when quantifiers can bind terms in function position, so are completely avoided in rigid ontologies.
Which of course suggests that it might be a good idea to restrict ourselves to the rigid case. That option remains: it would be very quick to do the necessary surgery, mostly by deletion.
A sequence variable stands for an 'arbitrary' sequence of arguments. Since
sequence variables are implicitly universally quantified, any toplevel expression
in which a sequence variable occurs has the same semantic import as the countably
infinite conjunction of all the expressions obtained by replacing the sequence
variable by a finite sequence of variables, all
universally quantified at the top level.
For example, the toplevel sentence R(@x)
occurring
in an ontology has the same meaning as the infinite conjunction
R() and (x)R(x) and (x)(y)R(x y) and (x)(y)(z)R(x y z)
Note . This includes the emptysequence case: to avoid this,
use a variable followed by a sequence variable: R(x @y)
.
Sequence variables can be used to write 'recursive' axiom schemes. Rather than attempt a fully general description of this technique, we will illustrate it with a canonical example. Consider the following sentences:
nil = list()
(x)(y)(z) not( x = list(@y) not cons(z x) = list(z @y) )
which have the same meaning as the infinite set of sentences:
(nil = list()
(x)(y)(z) not( x = list() not
cons(z x) = list(z) )
(x)(y)(z)(x1) not( x = list(x1) not cons(z x) = list(z x1) )
(x)(y)(z)(x1)(x2) not( x = list(x1 x2) not cons(z x) = list(z x1 x2) )
(x)(y)(z)(x1)(x2)(x3) not( x = list(x1 x2 x3) not cons(z x) = list(z x1 x2 x3)
)
...
(x)(y)(z)(x1)(x2)...(xn) not( x = list(x1 ... xn) not cons(z x) = list(z x1 ...
xn) )
... )
which clearly entails for any finite sequence t1... tn of terms, that
cons(t1 cons(t2 cons(...cons(tn nil)...)) = list(t1
... tn)
and thus provides the familiar technique of writing a list as a constructed Sexpression, first used in LISP and more recently as the RDF 'collection' vocabulary [refRDF]. The tailrecursion represented by the axiom is reexpressed here as induction on the length of a proof.
This general technique of imitating tailrecursive definitions by writing them as implications using sequence variables was pioneered by KIF [refKIF] and is one of the primary uses for sequence variables in SCL. What this construction shows, however, is that the use of sequence variables can be replaced, when required, by the use of explicit consnil lists as arguments, represented in SCL by nested terms.
Note that the fitting conditions on sequence variables require that list have every arity, i.e. that
(x) not (scl:Integer(x) not scl:Arity(x list))
S entails T when every interpretation which satisfies S also satisfies T.
An unfit ontology entails any other ontology, trivially. For plain ontologies, which can be identified with sets of SCL sentences, entailment behaves as usual and has conventional properties; and it also behaves as one would expect when the body of T fits the header of S. In other cases, however, the presence of headers can introduce some extra complications.
If ontologies have different headers  so are defined on different signatures, in effect  then entailment can be blocked solely by the requirements of syntactic fitting. For example:
(ontology P = ( ( not scl:Rel(f) ) :: ( a = a ) ))
(ontology Q = ( ( ) :: ( f(a) = f(a) ) ))
both P and Q have tautologous bodies, but P does not entail Q because Q uses a name in function position which the header of P asserts not to be a relation; so any interpretation which satisfies P will not fit Q, and therefore cannot satisfy Q.
One simple sufficient condition can be stated directly: If (H::P) is fit, then (H::P) entails (K::Q) when H entails K and P entails Q and also (H::Q) is fit. In particular, a fit ontology (H::P) entails (H::Q) iff H fits Q and P entails Q.
More interesting cases of entailment are provided by transformations between ontologies, in particular by header absorption.
Consider a named fit ontology (ontology n=(H::B)) and a satisfying interpretation I, with an expansion J which satisfies H. Seen as it were from the perspective of J, the quantifiers in B are interpreted as restricted to a subset of the universe of J. We can axiomatize this intuition directly by constructing an ontology which is like B except that a new unary predicate is introduced which identifies the universe of B, corresponding to scl:Ind in the header H, and restricting all quantifiers and names to this universe predicate. By convention we will use the name of the ontology as the predicate name, so that it refers to the 'universe of' the ontology. Formally, then, define B' as follows: for every expression in B containing a universal quantifier, let B' contain the expression obtained by replacing each universal quantified subexpression (var)body by the corresponding expression (var)not(n(var) not [body]) , where [body] is the transform of body; and for every name N in object position in B, let B' contain the atomic sentence n(N).
more to come
LEFTOVERSspecial namesQuoted strings begin and end with a singlequote character, and may contain any unicode character except that the singlequote character and the backslash character must be preceded by a single backslash character. A quoted string denotes the character string obtained by removing the outer single quote symbols and removing every occurrence of a backslash preceding a single quote or another backslash. Typed literals consist of a URI reference indicating a datatype and a string which is a valid lexical form for the datatype; the literal denotes the corresponding datatype value. SCL follows the RDF Ntriples notation for typed literals [refRDFSyntax].URI references (including URIs) are a special case. At the time of writing, it seems clear that URI references will continue to be widely used to refer to particular named entities in public use on the WWWeb, such as datatypes [ref XSD, refRDFMT], namespaces and the like, including such essentially 'network' entities as email destinations and websites. In particular, the basic architecture of the Web relies on a firm connection between URIs in the form of http: resource locators and the web 'resources' that they are used to access. It seems reasonable therefore to treat URIs as special names having an externally defined meaning. On the other hand, this meaning  unlike, say, the interpretation of numerals  is partial, labile and unreliable. Not all URIs have any assigned meaning, many apparently denote in a timedependent way, and the process of determining the denotation is inherently dependent on the global state of the Web. Even the most firmly anchored meanings, such as those of URNs established by published conventions and international registration conventions [refURN], hardly qualify as necessarily denoting their intended meanings: they are subject to social agreements and are prone to change with time and circumstances. Moreover, the architectural accounts of how 'web meaning' are determined even in an idealized sense are not yet firmly established [refChoreoArchive] and clearly require complex analysis [refREST]. Rather than wait on a future definitive theory of web reference, SCL takes the pragmatic view that any particular set of URI references may be considered to be special names by any application which is able to recognize them as having a fixed meaning; and that all other URI references should be considered simply to be names. This allows 'unallocated' URI references to be used freely as SCL constants, in the style used by the W3C standard Semantic Web formalisms RDF [refRDF] and OWL [refOWL]. Obviously, caution should be used when using URI references that may be assigned a special meaning in ways which are beyond the control of the user. SCL allows constants to be used as names of ontologies. In practice, we expect that these will frequently be URI references whose body URI is the URL of a document containing an SCL definition of the ontology written using XML notation, following the emerging semantic web practice. SCL itself takes no position on the exact form for ontology names, however.