SCL: Simple Common Logic

*** 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 role-set 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 truth-recursion, 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. Skin-defining framework. (use AS as a general skin-describing 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 header-elimination by guarding quantifiers, apply to FOL headers
5. provide some standard headers for importing, including lists and FOL-style headers. easy
6. Draft XML interchange syntax which does the defining properly, and allows markup to be mixed with non-SCL text. HARD
7. Describe holds/app embedding for generic SCL. SLOW
8. Handle Tanel's 2-equalities 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.

Contents

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

Introduction

This whole section probably needs rewriting eventually.

SCL is a first-order logical language intended for information exchange and transmission. SCL allows for a variety of different syntactic forms, called skins, all expressible within a common XML-based syntax and all sharing a single semantics. SCL is also self-contained 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 'higher-order' constructions such as quantification over classes or relations, and a semantics which allows theories to describe intensional entities such as propositions or properties. Conventional first-order syntactic forms can be defined in SCL by restricting the signature.

SCL can be embedded within a conventional first-order logical theory using a commonly-used translation, allowing existing first-order reasoners to be used as conforming SCL engines with minimal change. Most extant syntactic variants of first-order logic can be transcribed into an SCL dialect using a generic style of syntactic transformation.

Discussion and overview

historical notes on KIF and original motivation of knowledge interchange; new role of semantic web.

Surface syntax.

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 text-book 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 KIF-like 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_xyG_y&EyB_xIAx

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 XML-based 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 general-purpose interchange notation and mark-up language for any conforming SCL syntax. Finally, a general technique for defining SCL skins in terms of an SCL abstract syntax is described.

Contextual signatures

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 first-order 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 context-free method of checking that all terms and atomic sentences will be well-formed, and allows the usual first-order semantics to be defined on any well-formed syntax in a context-free 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 built-in 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 first-order 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.

Type-free syntax

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 relation-valued functions, or relations applied to other relations. The resulting syntax is similar to a higher-order syntax; but unlike traditional omega-order logic, SCL syntax is completely type-free. It requires no allocation of higher types to functionals, and imposes no type discipline. Self-application 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 truth-value, i.e. a proposition. Note the distinction between R() and R: the former denotes a truth-value; 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 'higher-order' syntax can be given a completely first-order semantics simply by refusing to countenance any logical comprehension principles, and allowing the universe of relations to be of arbitrary size. SCL is semantically first-order in this sense, and satisfies all the usual semantic criteria for a first-order language, such as compactness and the Skolem-Lowenheim property. SCL syntax can be uniformly translated into a conventional first-order theory using a conventional syntax defined by a simple signature. This 'holds-app' 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.

Functions and relations

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 2-functional 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 well-defined 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

Sequences and sequence variables

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 four-place relation between persons, marrying authorities and time-periods, 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 first-order axiom scheme, standing in for a countably infinite set of first-order 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 first-order 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 first-order logic, and for example is not compact [refHayMenzel]. The restrictions on sequence variables in SCL have been chosen to restrict the language to first-order 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

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 first-order 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 context-free manner.

SCL kernel, outline

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 set-based 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 top-level 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 type-free 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.

Sequences

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 truth-value true.

As noted earlier, SCL treats functions as a special class of functional relations. A set of finite sequences over U is n-ary 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.

SCL kernel formal syntax

The formal syntax of the kernel is g

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).

Position

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.

Special Cases

Several special cases of the kernel syntax can be identified, largely by restrictions on the syntax of atomic sentences and terms.

An ontology is first-order 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 first-order 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 fixed-arity.

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 first-order 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 Core skin

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 syntax-mapping business is done rather informally and in an ad-hoc fashion. Future drafts will provide a more precise technique for defining alternative syntax skins, maybe using an existing system of syntax-describing 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.

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 meta-varaibles indicating syntactic parts of an expression. Sequences of expressions are indicated using a conventional three-dots 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 role-set atom, and to ensure that the deMorgan translation of a disjunction is carried out properly.

Most of this is a standard translation of conventional logical notation into the and-not-forall 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 'role-set' syntax for atoms as an alternative to the argument-sequence syntax. Atomic sentences of the form

Married{wife=Jill husband=Jack}

are considered to take a set of arguments in the form of role-value pairs. (The skinning table assumes that this set has been ordered in some arbitrary way.) In this role-set 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 argument-order 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 role-names as selectors on the elements of this sequence. Under the presumption that role-values 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 argument-sequence 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 role-pairs 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 role-set 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:

SCL kernel semantics

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 signature-fitting 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:

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 first-order interpretation of the relation name: a conventional first-order 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.)

The truth-condition 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 top-level truth-conditions over-ride 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 context-free 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 truth-values, 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.

Kernel Features: discussion

SCL header vocabulary; fit and unfit ontologies

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 'mis-used' 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 first-order 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 first-order 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 first-order 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.

Importing and naming

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)
)

Fitting functions

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 truth-conditions 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 non-empty, 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.

Sequence variables and recursion

A sequence variable stands for an 'arbitrary' sequence of arguments. Since sequence variables are implicitly universally quantified, any top-level 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 top-level 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 empty-sequence 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 S-expression, first used in LISP and more recently as the RDF 'collection' vocabulary [refRDF]. The tail-recursion represented by the axiom is re-expressed here as induction on the length of a proof.

This general technique of imitating tail-recursive 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 cons-nil 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))

SCL entailment

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.

Absorbing headers

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

-------------------

END OF DOCUMENT

LEFTOVERSspecial namesQuoted strings begin and end with a single-quote character, and may contain any unicode character except that the single-quote 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 N-triples 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 e-mail 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 time-dependent 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.