1. 'abstract' syntax for SCL (structural BNF ignoring surface syntactic forms): + indicates a generic syntactic association (which might be indicated in various ways in different surface syntaxes); * indicates repetition; [ ] indicates optionals; terminals in italics.
module ::= [name +] [ header +] text
header ::= text
text ::= phrase*
phrase ::= sentence | import + name | comment
sentence::= quantifiedsentence | booleansentence | atom | comment + sentence
quantifiedsentence ::= quantifier [+ guard] + variablelist + sentence
quantifier ::= forall | exists
variablelist ::= (name | name + sort)*
booleansentence ::= and + sentence* | or + sentence* | implies + sentence + sentence | iff + sentence + sentence | not + sentence
atom ::= equal + term +term | relation + relarguments
relarguments ::= term* [+ seqvariable] | (role + term)*
term ::= name | function + term* [+ seqvariable] | comment + term
Quantifier guards, sorts in quantifier lists and role names in role-pair atomic syntax must be interpretable as relations, so:
guard ::= sort ::= role ::= relation
Full SCL allows relations and functions to be terms, but distinguishes a special category of atoms and terms in which the operator must be a simple name which is required to not denote anything in the domain of quantification, so any expression in which such a name is bound by a quantifier is illegal/unsatisfiable (take your pick). The nondenoting forms correspond most closely to conventional FO logic syntax, but introduce difficulties when used in a network context.
relation ::= function ::= term | nondenotingoperator
nondenotingoperator ::= name
Names are the basic terminal syntactic class. An SCL vocabulary is a set of names. There is no lexical distinction between function, relation and individual names (i.e. 'punning' is allowed.) In the current version there is no lexical distinction between names and variables: a variable in any expression is simply any name which is bound by a quantifier in a superexpression (this aspect of the design is under discussion.)
There is no restriction on the form of names: a names may be any Unicode string, but SCL recognizes numerals and quoted strings as special names with fixed interpretations (in effect, built-in datatypes), and names beginning with three dots '...' are treated as sequence variables in phrases (this was @ in KIF)
Headers are an optional device to allow an ontology to describe aspects of its own universe of discourse, to allow more nuanced relationships between ontologies. In a named ontology, the header text is understood to be stated in a global context where all names denote and the universe of quantification cannot be restricted or bounded; the remaining text is understood to be asserted in a local context where the universe of discourse is the relational extension of the ontology name. The local domain of quantification may be smaller than the global one. To move sentences from a local to the global context, all names must be asserted to be in the local domain and all quantifiers guarded by the local domain name. Note that ontology names are optional, so SCL can be used to transmit logical text without any reference to this machinery if required.
Quite a lot of this syntax can be considered as syntactic sugar. In particular, quantifier guards, the role-set atom syntax and the sorted quantifiers can be easily eliminated. The sequence variables can be encoded using lists or the RDF collection vocabulary, and are only needed for handling variadic relations/functions in any case.
For examples of the 'core' syntax, which is designed to be close to KIF, see
http://www.ihmc.us/users/phayes/SCLJune2004.html
General philosophy: direct use of XML to express syntax, rather than 'striped' technique. Logical structure exhibited directly in parent/child structure of elements; names are rendered as PCDATA ; generic syntactic categories provided to allow extensibility; linked to external syntax specifications by attributes.
NOTE. The particular element tags and indeed much of the 'XML design' of this syntax is open to discussion and negotiation, and has not yet been fully discussed within the SCL group itself. Please pay more attention to the structural aspects of the design. Thanks.
<comment> </comment>
Inserts a comment. Comment elements can be inserted anywhere inside any SCL element and are considered to be 'attached' to the immediate parent element. Comment elements can comprise any text, can be mixed content, and can have any user-defined attributes; they are ignored by logical processors, but conforming SCL applications are required to preserve them and their position relative to other elements. Comments inside other comments are considered to be comments on the comment; to add comments, place new comment elements adjacent to the comment. Note that SCL text inside a comment is not considered to be part of the SCL containing element.
Several elements also allow comments as attribute values; this allows comments to be attached to in-line SCL text without altering the syntactic form of the text, where this is required.
<scl> </scl>
Used to surround any piece of SCL content, to mark it off from other content in a document. Text inside this element should be legal SCL. It need not be a module (ontology).
attributes:
dialect
(optional) Indicates that the PCDATA in the element is SCL written in a particular dialect. This is used to include SCL text written in a non-XML dialect within legal XCL. For example, this is a legal SCL element:
<scl dialect="scl:core">
(forall ex:romanceNovel ((x man)) (exists ((y woman)) (and (loves x y) (not (loves y x))) ))</scl>
If this attribute is present then the body of the element should not be treated as mixed content.
The element may contain other user-defined attributes.
children:
<module> </module>
(optional)
<phrase> </phrase>
(optional) Used to indicate a top-level sentence in SCL text. The child element should be a single sentence element. This element may be omitted, and the sentence element incorporated directly in the text.
<comment> </comment>
(optional) inserts a comment.
----------
<module> </module>
Indicates that the enclosed text is considered to be an module (aka ontology). An SCL module is a piece of SCL text which has special attributes and satisfies certain extra constraints. Normally a piece of SCL content will comprise a single module, so this element, if present, will be the single child element of the <scl>
element; but this is not required.
attributes:
moduleName
(required) Used to assign an 'importing name' to a module. Normally this will be a URI reference, and often it will be the same as the xmlns default namespace and/or the URL of the containing document. However, this coincidence of naming is not required. No logical relationship is assumed between names based on their URI or XML namespace structure, so it is acceptable to use a URI reference containing a fragID to name an ontology. One document may contain several modules named with URI references formed from the URI of the document itself. (Intuitively, rather than being required to be the absolute URI of a namespace, the ontology importing name may be treated like other names in a namespace. This allows one ontology to treat another ontology as an entity in its namespace.)
dialect
(optional) Indicates that the PCDATA in the element is SCL written in a particular dialect.
children:
<import />
(optional)
<nothings> </nothings>
(optional)
<phrase> </phrase>
(optional)
<comment> </comment>
(optional)
------------
<phrase> </phrase>
Used to indicate a top-level sentence in SCL text. The single child element should be a sentence element. This element may be omitted, and the sentence element incorporated directly in the text.
attributes:
dialect
(optional) Indicates that the PCDATA in the element is SCL written in a particular dialect. This overrides any enclosing dialect attributes on parent elements; however, such clashes between parent and child dialect values are deprecated.
-----------
<import source="..." />
Empty element used to import one module into another. The value of the attribute should be the module name of an SCL module.
attributes:
The dialect
attribute may optionally be included in an import
element to indicate that the source should be encoded in that dialect. Conforming applications which find the SCL source to be encoded in a different dialect than the one indicated may either treat this as an error condition, or translate the source into the indicated dialect.
This element has no child elements.
-----------
<nothings> </nothings>
The PCDATA in this element is a sequence of SCL names. This element is used to indicate that these names do not denote 'things' in the current ontology, i.e. that they are nondenotingoperators
not included in the local domain of quantification. This allows an ontology to have strict control over the size of its intended domain of discourse. Names not listed in such a header are treated as denoting names in the ontology.
Nondenoting names can be used only in the relation or function position of atoms and terms in this module. They cannot be used as arguments or be bound by quantifiers in this module. Note however that a name may be nondenoting in one ontology but denoting in another ontology: the assignment of nondenoting status is local to this module.
This element has no attributes and no child elements.
The dialect
attribute should not be used inside a sentence element.
lfo
Any sentence element may have the attribute lfo
(logical form of) whose value is some content (usually a URIreference) which indicates a syntactic category in some external language specification. This is intended to indicate that the sentence is the result of a content-preserving translation into SCL of the syntactic form indicated. Any lfo
attributes of subelements of this element should indicate the appropriate categories of subexpressions of the external expression. For example, a Horn rule might appear in SCL as a univerally quantified implication between a conjunction and an atom; the lfo
value of the <forall>
might be "rulespec:hornrule", and that of the internal conjunction and atomic conclusion might then be "rulespec:body" and "rulespec:head". Only one 'external' translation can be specified for a given piece of SCL. To indicate that a single SCL sentence is the logical form of two distinct external syntaxes, it is necessary to write it twice, with suitable lfo
values for each external specification. (The repetition may be indicated by the use of XML standards external to SCL.) Currently there are no such external mappings defined.
syntaxtype
Quantified and boolean sentences can be stated 'generically' with the attribute syntaxtype
whose value is some content (usually a URIreference) which specifies or indicates the appropriate logical form. This attribute is provided for extensibility, to allow the inclusion of alternative logical syntax forms or patterns, eg numerical quantifiers or alternative boolean operators such as a binary conjunction or a Scheffer stroke. Currently there are no such extensions defined.
The attribute syntaxtype
cannot be used with the normal SCL quantifier and boolean sentence elements, which can be viewed as abbreviations of generic elements with scl:-prefixed properties, eg
<forall>...</forall>
abbreviates
<quantifiedSentence syntaxtype="scl:forall">...</quantifiedSentence>
<forall> </forall>
<exists> </exists>
These both enclose a quantified sentence and indicate the quantifier. The alternative generic form is
<quantifiedSentence syntaxtype="...."></quantifiedSentence>
attributes:
lfo
(optional)
children:
<guard></guard>
(optional; unique)
<bvar></bvar>
(required)
[any sentence element] (required; unique)
<comment> </comment>
(optional)
------------
<guard> </guard>
This optional element contains a name which is used as the guard of the quantifier, if present. This has no attributes and no children. It is used only inside a quantifier element, and must be the first child element if present.
------------
<bvar> </bvar>
Encloses a name bound by a quantifier. This must be a denoting name.
attributes:
sort
(optional). Value must be a name indicating the sort of the variable. This can be a nondenoting name.
No children.
------------
<and> </and>
<or> </or>
<implies> </implies>
<iff> </iff>
<not> </not>
These all enclose boolean sentences and indicate the truth-function. The alternative generic form is
<booleanSentence syntaxtype="...."> </booleanSentence>
The only one of these which is order-sensitive is implies
. By convention, the first child element is the antecendent, the second is the conclusion. (SCL does not require 'role' elements for boolean sentences, eg antecedent/conclusion.)
children:
Any boolean sentence element can have children of any sentence type. And
and or
take any number of children (including zero); implies
and iff
take two, and not
takes one.
<comment></comment>
(optional)
attributes:
lfo
(optional)
------------
<holds> </holds>
Atomic sentence indicating that a relation holds true of some arguments. The first child element always indicates the relation; this may be a nondenoting name. SCL allows two distinct forms for specifying arguments of a relation, as an ordered list or as a collection of role-value pairs. The latter form is indicated by the attribute syntaxtype
on the holds element with the value roleset
.
attributes:
lfo
(optional)
syntaxtype (
optional)
children:
One <rel>
element (required)
either:
some number (maybe zero) of <name>
or <app>
elements;
or:
some number (maybe zero) of <role>
elements.
<comment> </comment>
(optional)
------------
<rel> </rel>
Encloses a name or a <app>
. The name may be nondenoting.
No attributes.
children:
<comment> </comment>
(optional)
<app> </app>
(optional: unique)
------------
<equal> </equal>
No attributes.
children:
exactly two <name>
or <app>
elements.
-----------
<role> </role>
attributes:
name
. (required) The value is a name which indicates the role of the content in the atom. Role names denote binary relations in SCL, and may be nondenoting.
The content of this element is a name or <app>
element indicating the argument 'filler' of the slot.
Example of an atom using the role syntax:
<holds syntaxtype="roleset"> <rel>married</rel>
<role name="wife">Jill</role>
<role name="husband">Jack</role>
</holds>
No children
------------
<app> </app>
Indicates a term obtained by applying a function to some arguments. The first child element denotes the function and can be a name or a term element. The name may be nondenoting.
No attributes.
children:
<fun> </fun>
(required; unique)
some number of <name>
or <app>
elements
<comment> </comment>
(optional)
------------
<fun> </fun>
Encloses a name or an <app>
. The name may be nondenoting.
No attributes.
children:
<comment> </comment>
(optional)
<app> </app>
(optional: unique)
------------
<name> </name>
Encloses a name. Permissible but redundant as the immediate child of a <guard>
, <bvar>
, <sort>
, <rel>
, <fun>
or <role>
element.
No attributes.
children:
<comment> </comment>
(optional)
-------------
Example 1. Rule ML 'owns' rule http://www.ruleml.org/indtd0.8.html#Context, full XCL form with external links to RuleML syntax. This is an XCL sentence:
<scl>
<forall lfo="http://www.ruleml.org/indtd0.8/rule">
<bvar>person</bvar>
<bvar>merchant</bvar>
<bvar>object</bvar>
<implies>
<and lfo="http://www.ruleml.org/indtd0.8/body">
<holds><rel>buy</rel>
<name>person</name>
<name>merchant</name>
<name>object</name>
</holds>
<holds><rel>keep</rel>
<name>person</name>
<name>object</name>
</holds>
</and>
<holds lfo="http://www.ruleml.org/indtd0.8/head"><rel>own</rel>
<name>person</name>
<name>object</name>
</holds>
</implies>
</forall>
</scl>
Using the core dialect, without external links but using comments to indicate the external relationships:
<scl dialect="scl:core">
(comment 'lfo="http://www.ruleml.org/indtd0.8/rule"'
(forall (person merchant object)
(implies
(comment 'lfo="http://www.ruleml.org/indtd0.8/body"'
(and (buy person merchant object)(keep person object)) )
(comment 'lfo="http://www.ruleml.org/indtd0.8/head"'
(own person object) )
)) )
</scl>
(Note, in the core syntax, comments 'wrap' the expressions they comment upon, so that (comment 'whatever' P )
is logically equivalent to P
. )
Example 2. Trailertrucks are eighteenwheelers (see http://www.daml.org/listarchive/joint-committee/1713.html )
<scl>
<forall>
<bvar>x</bvar>
<implies>
<holds><rel>TrailerTruck</rel>
<name>x</name>
</holds>
<holds><rel>EighteenWheeler</rel>
<name>x</name>
</holds>
</implies>
</forall>
</scl>
using core dialect:
<scl dialect="scl:core"> (forall (x) (implies (TrailerTruck x)(EighteenWheeler x))) </scl>
Logically equivalent forms using sorts in the quantifier:
<scl>
<forall>
<bvar sort="TrailerTruck">x</bvar>
<holds><rel>EighteenWheeler</rel>
<name>x</name>
</holds>
</forall>
</scl>
<scl dialect="scl:core"> (forall (x TrailerTruck)(EighteenWheeler x)) </scl>