Note: SCL also has ontology-level syntax to define modules (=ontologies), name them, import them, etc.. This is ignored in this document.
(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.
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
relation ::= function ::= term
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). This is handled in the XCL syntax by listing them explicitly as 'no-thing' names. The nondenoting forms correspond most closely to conventional FO logic syntax, but introduce difficulties when used in a network context.
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 (single-)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 the core syntax (this was @ in KIF). The XCL syntax ignores sequence variables.
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 details of the 'core' syntax, which is designed to be close to KIF, see
http://www.ihmc.us/users/phayes/SCLJune2004.html
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.
<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.
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 legal XCL:
<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 dialect attribute should not be used inside a sentence element.
The element may contain other user-defined attributes.
children:
<nothings> </nothings> (optional)
any sentence element (optional)
<comment> </comment> (optional)
----------
<nothings> </nothings>
This element is used to indicate that some 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.
children:
<name> </name>
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 .
A seqvar, if present, indicates an axiom schema which covers an infinite collection of FO instances, one for each possible arity. See here for a discussion of sequence variables.
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.
One <seqvar> </seqvar> (optional: unique)
<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)
------------
<seqvar> </seqvar>
Contains a name indicating a sequence variable.
No attributes or children.
------------
<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.
A seqvar, if present, indicates an axiom schema which covers an infinite collection of FO instances, one for each possible arity. See here for a discussion of sequence variables.
No attributes.
children:
<fun> </fun> (required; unique)
some number of <name> or <app> elements
One <seqvar> </seqvar> (optional: unique)
<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>
using core dialect:
<scl dialect="scl:core"> (forall (x TrailerTruck)(EighteenWheeler x)) </scl>
Example 3. Example 1 re-written using roles for atomic sentences. The external lfo links have been removed as they are no longer exactly correct. Since this introduces explicit role names, it has a more complex logical form than the first example :
<scl>
<forall >
<bvar>person</bvar>
<bvar>merchant</bvar>
<bvar>object</bvar>
<implies>
<and >
<holds syntaxtype="roleset"><rel>buy</rel>
<role name="buyer">person</role>
<role name="seller">merchant</role>
<role name="boughtThing">object</role>
</holds>
<holds syntaxtype="roleset"><rel>keep</rel>
<role name="keeper">person</name>
<role name="kept">object</name>
</holds>
</and>
<holds syntaxtype="roleset"><rel>own</rel>
<role name="owner">person</name>
<role name="owned">object</name>
</holds>
</implies>
</forall>
</scl>
Expressed in the core dialect and with the role-set sugar replaced by its underlying logical form, this is equivalent to:
<scl dialect="scl:core">
(forall (person merchant object)
(implies
(and
(exists (x)(and (buy x)(buyer x person)(seller x merchant)(boughtThing x object)))
(exists (y)(and (keep y)(keeper y person)(kept y object) ))
)
(exists (z)(and (own z)(owner z person)(owned z object)))
)
)
</scl>
which would of course be rather longer if written out in full XCL element form.