[SCL] Second version of the SCL draft spec here
pat hayes
phayes at ihmc.us
Tue Nov 4 14:27:47 CST 2003
><x-flowed>Hi,
>
>After both reading the discussion from the last few days and
>doing some additional thinking, I have made some modifications
>and additions to the SCL draft spec.
>
>The new spec (1. november) is attached.
>
>Please look at the "Appendix D: changes from
>the previous version" first: the modifications
>and additions are enumerated and described
>there.
>
>In particular, I have written chapters on SCL
>abstract syntax and SCL->traditional FOL
>translation.
>
>The first of these is NOT intended to replace
>Chris's earlier SCL abstract syntax, but rather
>to push him towards producing a simpler-to-read
>presentation with some complex ascpects
>like "SCL languages" dependent on lexicon
>simply removed.
I agree that this would be a good idea, but I
still want us to provide a genuinely abstract
syntax for SCL. 'Abstract' here means a lot more
than just ignoring things like whitespace. For
example, in an AS, there is no such thing as a
quantifier symbol, since some concrete syntax
forms indicate quantification diagrammatically.
The use of a quantifier symbol is only one style
of indicating a quantified sentence form in a
concrete syntax.
I like the 'core'/'modules' organization, though
I wonder if we can honestly call equality a
module in this sense.
Chris, how are you coming along? Should I try to write up an AS section?
Pat
>Please feel free to replace the new
>abstract syntax chapter with your own,
>provided it is not more complex than
>the one I just produced. Any changes
>to the current one, merges, etc are
>also fine, of course.
>
>Regards,
> Tanel Tammet
>
>
>
>
>
></x-flowed>
><x-html><!x-stuff-for-pete base="" src="" id="0"
>charset="iso-8859-1/macintosh"><!DOCTYPE HTML
>PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
><html>
><head>
> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
> <style type="text/css">
> body { color: black; background: white; }
> body { font-family: Times, serif}
> body { margin: 0px 80px 0px 80px}
> A:link {color: blue}
> A:active {color: red; font-weight: bold}
> A:visited {color: "red"}
> </style>
> <title>SCL Model and Syntax</title>
></head>
>
><body>
>
><center>
><h1>Simple Common Logic<br>
>(SCL) Model and Syntax Specification</h1>
>
><h3>SCL working group: work in progress</h3>
></center>
>
><dl>
><dt>This Version:</dt>
><dt>
>1. nov 2003, submitted by T.Tammet (see <a href="#changes">Appendix D</a>
>for changes and versioning information).
></dt>
>
><dt>Newest Version:</dt>
><dt><em>.. to be filled ...</em>
></dt>
>
><dt>Editors:</dt>
><dt><em>... to be filled ...</em>
></dt>
></dl>
>
><h2>Status of This Document</h2>
>
><p>This document is an early draft of the informal SCL working group. Work on
>this document is in progress. The future versions of this document are
>intended to be used as a normative reference. The current verson of this
>document is not intended to be normative.</p>
>
><p>Comments on this specification may be sent to
><a href="mailto:www-rdf-comments at w3.org">scl at philebus.tamu.edu</a>. The
>archive of public comments and SCL discussion is available at
><a
>href="http://www.w3.org/Archives/Public/www-rdf-comments">http://philebus.tamu.edu/mailman/listinfo/scl</a></p>
>
><h2><a name="TOC"></a>Table of Contents</h2>
>
><ol>
> <li><a href="#intro">Introduction</a></li>
> <li><a href="#principles">Basic principles of SCL</a></li>
> <li><a href="#context">SCL in the context of FOL, KIF, RDF and OWL</a></li>
> <li><a href="#abstract">SCL core abstract syntax</a></li>
> <li><a href="#sclinformalkifcore">Informal
>SCL/KIF concrete syntax for core SCL</a></li>
> <li><a href="#modelfol">Translation of core
>SCL to FOL: semantics via FOL</a></li>
> <li><a href="#modelstandalone">Standalone semantics of core SCL</a></li>
>
> <li><a href="#fullscl">Full SCL modules</a></li>
> <ol>
> <li><a href="#scannot">SCL-ANNOT: annotations</a></li>
> <li><a href="#sclrole">SCL-ROLE: role symbols</a></li>
> <li><a href="#sclrestquant">SCL-RESTQUANT:
>restricted quantifiers</a></li>
> <li><a href="#scleq">SCL-EQ: equality</a></li>
> <li><a href="#sclint">SCL-INT: integers</a></li>
> <li><a href="#sclstring">SCL-STRING: strings</a></li>
> <li><a href="#scllist">SCL-LIST: lists</a></li>
> <li><a href="#sclseqvar">SCL-SEQVAR: sequence variables</a></li>
> </ol>
> <li><a href="#syntaxes">Concrete syntaxes</a></li>
> <ol>
> <li><a href="#sclprefix">SCL/PREFIX concrete syntax</a></li>
> <li><a href="#sclkif">SCL/KIF concrete syntax</a></li>
> <li><a href="#sclxml">SCL/XML concrete syntax</a></li>
> <li><a href="#scln3">SCL/N3 concrete syntax</a></li>
> </ol>
> <li><a href="#examples">Larger examples</a></li>
> <li><a href="#scltordf">Translation example: RDF translation to SCL</a></li>
> <li><a href="#acknowledgements">Acknowledgements</a></li>
> <li><a href="#glossary">Appendix A: Glossary</a></li>
> <li><a href="#usage">Appendix B: Notes about Usage</a></li>
> <li><a href="#references">Appendix C: References</a></li>
> <li><a href="#changes">Appendix D: Changes From Previous Version</a></li>
></ol>
>
><h2><a name="intro">Introduction</a></h2>
>
><p>Simple Common Logic (SCL) is a formal
>language for <i>knowledge interchange</i>
>among various software systems. SCL is basically a fully formalised,
>concrete version of classical first order logic (FOL),
>containing several conventions which are widely used in practical,
>logic-based application languages, while not always present
>in "textbook" versions of FOL.</p>
>
><p>SCL is intended to be "simple" in the sense that it contains only
>a few, widely used conventions and extensions to "textbook" FOL
>versions. SCL is not aimed to cover all kinds of extensions and conventions
>used in real world. Rather, it is targeted to be a "common denominator"
>on which necessary extensions can be easily built as need arises.</p>
>
><p>The problem of knowledge interchange among software systems
>has been a serious obstacle to efficient design of large systems
>for decades. A number of standards has been proposed and used,
>with increasingly more expressive and more complex structure.</p>
>
><p>Due to the explosive growth of network systems during the last decade,
>this problem has become more important than ever. Special fields of
>computer science have emerged, with the goal to create specialised,
>yet widely usable and standardised languages and software tools for
>knowledge interchange between systems. The areas of
><a href="http://www.w3c.org/2001/sw/">Semantic Web</a> and
><a href="http://www.w3c.org/2002/ws/">Web Services</a> are perhaps
>most well-known among these fields.</p>
>
><p>A large subset of the existing and worked-on languages and tools
>for knowledge interchange is based on classical first order logic (FOL):
>typically, some subset or a superset of FOL along with special axiomatisations
>and special syntax is used as a core of these languages.</p>
>
><p>The <i>Simple Common Logic (SCL)</i> language presented in this
>specification is intended to be used as:</p>
>
><ul>
><li>An underlying, common core language for specifying meanings (semantics)
> of several application-oriented languages.</li>
><li>As a basis for building new languages,
>providing either further extensions
> and expressivity or useful properties for query answering, deduction,
> specialised application areas, etc.</li>
><li>As a standardised version of FOL, useful in various areas apart from
> pure knowledge interchange, like deductive databases, automated theorem
> proving, etc.</li>
></ul>
>
><p>Classical first order logic (FOL) has been a
>cornerstone of a wide spectrum of
>applications of logics for a long period of time.</p>
>
><p>However, the SCL working group fully
>recognises that FOL may not be sufficient
>for all kinds of specialised tasks, which may require, for example,
>variations of modal logic, nonmonotonic logics, etc. However, most of
>these logics contain FOL, thus a standardised version of FOL would be
>useful also in contexts requiring operators not present in FOL.</p>
>
><p>Similar reasoning applies in cases the specialised languages are
>much weaker than FOL (for example, RDF and Datalog). Although these
>languages do not need or want the full power of FOL, they are typically
>based on some restricted subclass of FOL.</p>
>
><h2><a name="principles">Basic principles of SCL</a></h2>
>
><p>When people speak or write about FOL, then the exact meaning of "FOL" is
>typically slightly different among participants of the conversation.
>Since the invention of FOL by Gerhard Gentzen in the nineteenth century,
>a number of variations of FOL have turned up. Some contain, for example,
>equality, while others do not. Syntax of "FOL" varies widely from
>textbook to textbook. </p>
>
><p>Hence, one of the goals of SCL is to present one fully specified
>abstract syntax along with semantics. Additionally, several fully
>specified concrete syntaxes (ordinary prefix syntax, KIF lisp-like syntax,
>XML syntax, N3 RDF-oriented syntax) are presented. New concrete
>syntaxes are easy to create along with the algorithms to translate
>from one syntax to another, while preserving the <i>meaning</i> of
>the translated text without any changes. </p>
>
><p>SCL is layered into the <b>core SCL</b> containing the very
>basics of FOL and <b>full SCL</b> containing a number of widely
>used conventions and extensions called <i>modules of SCL</i>.
>The modules are either syntactic constructs (syntactic sugar or
>"macro" operators) or built-in predicates and functions with a
>defined meaning in SCL.</p>
>
><p>The core SCL does not contain any syntactic sugar or
>built-in, defined predicates or functions. As such, it has to be extended
>for being usable in practical applications and for giving
>meaning to specialised languages.</p>
>
><p>The extensions present in full SCL are independent of each other:
>an implementation based on SCL may
>choose to implement either full SCL, just the core SCL or core SCL
>plus one or two modules. It is crucial, however, that any such
>implementation clearly identifies the layer and/or modules of SCL
>it implements.</p>
>
><p>For people familiar with some form of a traditional "textbook" FOL,
>the major difference of SCL from "traditional" FOL is the fact that
>SCL allows predicates and functions to be quantified over, essentially
>treating them as ordinary FOL constants. This does <b>not</b> mean
>that SCL uses any higher-order constructions. Rather, this convention
>simplifies the language, removing a somewhat artificial difference
>between predicate symbols, function symbols and constant symbols,
>along with the practical problems associated with the arity of predicate
>and function symbols</p>
>
><p>The main reason for treating predicate and function symbols in the
>same way as constants stems from the requirements of practical
>systems built on some form of FOL. For example, in the PROLOG
>programming language it is possible to use constructions matching
>predicates with a variable. Similarly, the RDF language of the Semantic
>Web requires that predicate symbols are treated as ordinary
>constants which may be matched with a variable. Earlier languages
>with similar goals to SCL (for example, KIF)
>have also adopted this practice.</p>
>
><p>Essentially, SCL treats logical axioms and
>terms as tuples with no principal
>difference between different positions of the
>elements in the tuple. Conventionally,
>the first element of a tuple is used as a predicate or function symbol in FOL,
>but this is a convention, not a requirement.</p>
>
><p>This simplified treatment of atoms and terms as tuples has some effects
>in regards to how such useful predicates like equality have to be axiomatised
>and treated. The tuple-treatment has no special effects on core SCL (which
>does not contain any specially defined predicates or functions), but
>it has to be taken account when axiomatising built-in predicates and functions
>of the full SCL. See the details in the following chapters.</p>
>
><p>The modules of full SCL are not meant to cover all possible needs
>of specialised applications. However, they do cover typical needs:
></p>
>
><ul>
> <li><b>Annotations</b> to formulas and terms.
>Annotations are basically slots
> in the syntax for adding both comments and metainformation to terms
> and formulas, which have no semantics defined in SCL. Annotations are
> defined as predicates and functions basically throwing away the
> "comment and metainformation" slot. However, in practical applications
> such annotations may convey crucial information, the syntax and
> semantics of which has to be given by the application itself, in
> a layer completely separate from SCL.</li>
>
> <li><b>Role symbols</b> is a syntactic feature allowing users to indicate
> the <i>name</i> of a position in a tuple, much like columns in a table
> of a typical RDBMS are indicated by the field
>name, not by the position number
> of the column. </li>
>
> <li><b>Restricted quantifiers</b> is a
>syntactic feature allowing users to indicate
> the type of the quantified variables in the
>quantification operator (exists,
> forall). The <i>type</i> in this context is determined by an ordinary
> predicate and the restricted quantifier construction is simply a shorthand
> for an ordinary quantifier and an implication where the restriction
> is a premise of the implication. No special
>type systems are introduced.</li>
>
> <li><b>Equality</b> predicate. Full SCL provides two equality predicates:
> one of them corresponds exactly to the ordinary equality predicate
> of traditional FOL versions, while the other is more powerful, stemming
> from the equal treatment of predicate, constant and function symbols.</li>
>
> <li><b>Integers</b> and some of the operations
>on integers are defined. Applications
> may easily define additional operations,
>using the basic operations provided by SCL.
> No attempts to provide a "full spectrum" of conventional integer operations
> are taken in SCL. In particular, SCL does not define any induction schemas:
> these have to be added in an additional layer by the applications using
> induction.</li>
>
> <li><b>Strings</b> and some of the basic
>operations on strings are defined, similarly
> to integers.</li>
>
> <li><b>Lists</b> and some of the basic
>operations on lists are defined, somewhat
>similarly
> to integers.</li>
>
> <li><b>Sequence</b> variables are defined.
><i>... needs to be filled in ....</i></li>
>
>
></ul>
>
><h2><a name="context">SCL in the context of FOL, KIF, RDF and OWL</a></h2>
>
><h2><a name="abstract">SCL core abstract syntax</a></h2>
>
><i>
><b>Warning: </b> This chapter is an <b>early</b> version,
>built by modifying Chris's earlier abstract syntax chapter.
>This chapter should be <b>replaced or modified</b> as soon as we get
>a new version of abstract syntax from Chris. The main purpose of this
>temporary/early chapter is to influence Chris and other people to present
>(a) syntax as easily readable as possible (b) altogether avoid the notion of
>"scl languages" in the sense that "Every SCL lexicon determines a class
>of languages". Instead, we should speak about (1) SCL layers (core and full,
>the latter containing several independent modules) (2) different concrete
>syntaxes. In the other words, we always assume that we have an unrestricted
>lexicon. T.Tammet.
></i>
>
><p>In this chapter we will present the syntax of core SCL. The syntax of full
>SCL adds some new constructions to the core SCL, but leaves the core SCL
>syntax unchanged. See the chapter on full SCL.</p>
>
><p>The syntax in this chapter is called "abstract" since we will not consider
>the issues related to white space, ASCII and UNICODE, and we do not consider
>the question of how a parser will differentiate
>one construction from the other.
>All these issues (highly relevant for both reading actual SCL text and
>building working parsers) are covered in the chapter of concrete syntaxes.
>As a quick preview of concrete syntaxes, the next chapter will demonstrate
>the basics of the SCL/KIF concrete syntax: how is the abstract syntax
>represented in the concrete SCL/KIF syntax.</p>
>
>
><h3>Primitives</h3>
>
><p>The SCL <i>primitives</i> is a basic set of
>primitive items in the language.
>It consists of:</p>
>
><ul>
> <li>An infinite set of <i>constants</i>.
> <li>An infinite set of <i>variables</i>.
> <li>A finite set of <i>connectives</i>.
> <li>A finite set of <i>quantifiers</i>.
></ul>
>
><p>In concrete SCL syntaxes it is allowed for one string (lexical item) to
>stand for both a constant, variable, connective or a quantifier primitive.
>The concrete type of a primitive in a concrete SCL syntax must be decidable
>either from the context or some concrete features of the lexical item.</p>
>
><h4>Connective primitives</h4>
>
><p>Each connective primitive <i>c</i> in SCL represents a connective in logic
>(negation, disjunction, etc) and is associated with an arity number:
><ul>
> <li><i>Arity(c)</i>: The allowed and required number of arguments to
> this connective primitive.
></ul>
>
><p>The finite set of connective primitives in SCL is the following:</p>
><ul>
> <li><i>Neg</i>: the negation connective. <i>Arity(Neg)=1</i>.
> <li><i>Conj</i>: the conjunction connective. <i>Arity(Conj)=2</i>.
> <li><i>Disj</i>: the disjunction connective. <i>Arity(Disj)=2</i>.
> <li><i>Imp</i>: the implication connective. <i>Arity(Imp)=2</i>.
> <li><i>Equiv</i>: the equivalence connective. <i>Arity(Equiv)=2</i>.
></ul>
>
><p>Any core or full SCL implementation should
>recognise all these connectives and be
>able to check the number of arguments.</p>
>
><p>Notice that it is possible to represent any logical connectives
>by formulas containing connectives <i>Neg</i> and <i>Disj</i>
>alone (other combinations are also possible). However, such representations
>are sometimes inconvenient, hence SCL requires that the connectives listed
>above are recognised by systems handling SCL. </p>
>
><h4>Quantifier primitives</h4>
>
><p>Each quantifier primitive <i>q</i> in SCL
>represents a quantifier in logic.</p>
>
><p>The finite set of quantifiers in SCL is the following:</p>
><ul>
> <li><i>Forall</i>: the "for all" quantifier.
> <li><i>Exists</i>: the "exists" quantifier.
></ul>
>
><p>Any core or full SCL implementation should
>recognise all these quantifiers.</p>
>
>
><h3>Constructions</h3>
>
><p>The <i>SCL constructions</i> are built from this set of primitives
>by additional <i>term</i>, <i>atom</i>, <i>formula</i> and <i>sequence</i>
>constructions. Each of these constructions is essentially either a primitive
>or a tuple of SCL constructions. The SCL abstract syntax uses functions
><i>Term_n</i>, <i>Atom_n</i>, <i>Formula_n</i> and <i>Sequence_n</i> to
>denote tuples of length <i>n</i> of a particular type. These functions
>are typically not included in concrete SCL syntaxes, where the type of
>a tuple is determined either by context or special syntactic features,
>different for each concrete syntax.</p>
>
><p>While the <i>term</i>, <i>atom</i> and <i>formula</i> constructions
>of SCL correspond to traditional FOL notions, the <i>sequence</i>
>construction stems from the practical necessities of software systems handling
>SCL text. A typical software system receives SCL text as either
>a file or a string of characters. It is convenient to allow such
>a file or a string to contain an arbitrary number of SCL constructions,
>one after another. For example, ordinary Prolog, Datalog, HTML etc
>software systems adopt this convention. The <i>sequence</i> construction
>in the SCL abstract syntax stands for such a
>representation. The <i>semantic</i>
>or meaning of the sequence conjunction is simply
>a logical conjunction of all the
>elements of the sequence tuple.</p>
>
><p>We will need to distinguish tuples for terms from
>tuples for atoms, formulas and sequences. As said, this distinction is done
>in different ways in different concrete syntaxes. In the abstract syntax
>we will employ the following convention:</p>
>
><ul>
> <li><b>Terms</b>. A <i>term</i> is a defined as being either
> <p>
> <ul>
> <li>a <i>constant</i> primitive, or
> <li>a <i>variable</i> primitive, or
> <li>a <i>complex term</i>.
> A <i>complex term</i> is defined as a construction
> <i>Term_n(e1,...,en)</i>, which is a tuple of <i>n</i> elements
> <i>e1,...,en</i>, where each <i>ei</i> is a <i>term</i>.</li>
> </ul></li>
> </p>
>
> <li><b>Atoms</b>. An <i>atom</i> is defined as being a construction
> <p>
> <i>Atom_n(e1,...,en)</i>, which is a tuple of <i>n</i> elements
> <i>e1,...,en</i>, where each <i>ei</i> is a <i>term</i>.
> </p>
>
> <li><b>Formulas</b>. A <i>formula</i> is defined as being a construction
> <p>
> <p><i>Formula_n(e1,...,en)</i>, which is a tuple of <i>n</i> elements
> <i>e1,...,en</i>, where the first element of a tuple, <i>e1</i>,
> is either a <i>connective</i> or a <i>quantifier</i> primitive.</p>
>
> <p>Additionally, there are following requirements on the tuple length
> and tuple element types, depending on
>whether <i>e1</i> is a <i>connective</i>
> or <i>quantifier</i> primitive:
>
> <ul>
> <li>Case where <b><i>e1</i> is a
><i>connective</i> primitive</b>:
> <ul>
> <li>The remaining elements of a tuple
><i>e2,...,en</i> are <i>formulas</i>.
> <li>The length of the tuple <i>n</i> is equal to <i>Arity(e1)+1</i>
> where <i>Arity(e1)</i> is the number of arguments, associated
> with this particular connective primitive <i>e1</i>.</li>
> </ul>
> </li>
> <li>Case where <b><i>e1</i> is a
><i>quantifier</i> primitive</b>:
> <ul>
> <li>The second element of a tuple <i>e2</i> is a tuple of
> <i>variable primitives</i> with, the
>tuple length one or bigger.
> <li>The third element of a tuple
><i>e3</i> is a <i>formula</i>.
> </ul>
> </li>
> </ul>
>
> </p>
>
> <li><b>Sequences</b>. A <i>sequence</i> is defined as being a construction
> <p>
> <i>Sequence_n(e1,...,en)</i>, which is a tuple of <i>n</i> elements
> <i>e1,...,en</i>, where each <i>ei</i> is a <i>formula</i>.
> </p></li>
>
></ul>
></p>
>
><h2><a name="sclinformalkifcore">Informal
>SCL/KIF concrete syntax for core SCL</a></h2>
>
>
><h2><a name="modelfol">Translation of core SCL
>to FOL: semantics via FOL</a></h2>
>
><i>
><b>Warning: </b> This chapter is an early version, based on the
>early/temporary chapters above and (loosely)
>Chris and Pat standalone semantics.
>This chapter should be <b>extensively
>modified</b> as soon as we get standalone
>semantics. Standalone semantics has to
>correspond <b>exactly</b> to FOL translation
>semantics: both of them can be modified towards
>each other as necessary. T.Tammet.
></i>
>
><p>After presenting both the abstract syntax of
>core SCL and giving an informal introduction
>to one particular concrete syntax of core SCL,
>we will now give exact <i>semantics</i>
>to the core SCL language, ie the <i>meaning</i>
>of SCL sentences. As is customary
>in logic, the meaning of SCL has mostly to do with computing the truth value
>of SCL sentences. The SCL semantics is essentially the same as the semantics
>of various traditional FOL versions.</p>
>
><p>We will present the semantics of SCL in two
>different ways, in two different
>chapters:
><ul>
> <li>By translating SCL to "traditional FOL".
>This is the approach of the current
> chapter.
> <li>By giving semantics to SCL without using
>the help of any other logical systems.
> This is the approach of the next chapter.
></ul>
>
><p>Both presentations of semantics give exactly
>the same results. The motivation
>for presenting semantics in two different ways stems from the following:
><ul>
> <li>Since there exists no concrete, standardised version of traditional FOL,
> the "translation to traditional FOL" approach is riddled with a danger
> of different interpretations, stemming from
>the various ways people understand
> "traditional" FOL. This danger is eliminated by the standalone semantics.
> <li>People accustomed to some form of traditional FOL may find it easier to
> understand the translation of SCL to FOL than the SCL standalone semantics.
> <li>There exist a number of automated theorem proving systems for traditional
> FOL. It is easier for the implementors and users of these systems to read,
> parse and use SCL for automated proof search
>if there is a concrete, normative
> translation to traditional FOL.
></ul>
></p>
>
><p>Observe that the translation presented in this chapter is defined for core
>SCL only. Translation of full SCL is presented stepwise in the chapters
>of modules of full SCL. </p>
>
><p>The overall scheme of translating SCL to
>traditional FOL is straightforward.
>The only issue to be taken into consideration is
>that most traditional FOL systems
>do not use the notion of a tuple. Instead, the
>constructions of traditional FOL are
>primitives, terms, atoms and formulas, where term is essentially a function
>application (for any kind of a function) and atom is essentially a predicate
>application (for any kind of a predicate).</p>
>
><p>Examples of traditional FOL:</p>
><p>
><ul>
> <li><b>Terms</b> may look like <i>f(a,X), g(X), m(g(X),f(1,X))</i> where
> <i>f, g, m</i> are special <i>function symbols</i> with a fixed arity,
> <i>a, 1</i> are <i>constant symbols</i> and
> <i>X</i> is assumed to be a variable symbol in the example
> (ie it is bound with a quantifier in some surrounding formula)
> <li><b>Atoms</b> may look like <i>P(a,X), R(X), P(g(X),f(1,X))</i> where
> <i>P, R</i> are special <i>predicate symbols</i> with a fixed arity,
> <i>f, g</i> are special <i>function symbols</i> with a fixed arity,
> <i>a, 1</i> are <i>constant symbols</i> and <i>X</i> is a variable symbol.
></ul>
></p>
>
><p>SCL, however, considers terms, atoms and formulas as being tuples of the
>corresponding type. There are no special function or predicate symbols, just
>constants and variables. The traditional FOL constructions from the previous
>example would - in the SCL abstract syntax - look like:
><ul>
> <li><b>Terms:</b>
> <ul>
> <li>FOL term <i>f(a,X)</i> in the SCL abstract syntax:
> <i>Term_3(f,a,X)</i> </li>
> <li>FOL term <i>g(X)</i> in the SCL abstract syntax:
> <i>Term_2(g,X)</i></li>
> <li>FOL term <i>m(g(X),f(1,X))</i> in the SCL abstract syntax:
> <i>Term_3(m,Term_2(g,X),Term_3(f,1,X))</i> </li>
> </ul>
> where
> <i>f, g, m, a, 1</i> in the SCL syntax are all <i>constant symbols</i>
> and <i>X</i> is assumed to be a variable symbol in the example
> (ie it is bound with a quantifier in some surrounding formula)
> </li>
>
> <li><b>Atoms:</b>
> <ul>
> <li>FOL atom <i>P(a,X)</i> in the SCL abstract syntax:
> <i>Atom_3(P,a,X)</i> </li>
> <li>FOL atom <i>R(X)</i> in the SCL abstract syntax:
> <i>Atom_2(R,X)</i></li>
> <li>FOL atom <i>P(g(X),f(1,X))</i> in the SCL abstract syntax:
> <i>Atom_3(P,Term_2(g,X),Term_3(f,1,X))</i> </li>
> </ul>
> where
> <i>P, R, f, g, m, a, 1</i> in the SCL syntax
>are all <i>constant symbols</i>
> and <i>X</i> is assumed to be a variable symbol in the example
> (ie it is bound with a quantifier in some surrounding formula)
></ul>
>
><p>Similarly, the traditional FOL <i>formulas</i> are applications of the
>connective functions, not tuples of the formula type, as in the SCL abstract
>syntax.</p>
>
><p>However, it is easy to see that we can translate SCL formulas to standard
>FOL by simply <b>removing the tuple
>constructor</b> and using the first element
>of a tuple as a function, predicate or connective function, with the rest of
>the tuple being arguments to this function.</p>
>
><p>Similarly, FOL formulas can be translated to the SCL abstract syntax by
><b>adding the tuple constructors</b> and mving the function, predicate
>and connective symbols to the additional first
>position of the argument tuple.</p>
>
><p>For simplicity, we assume that the
>particular version of traditional FOL we
>translate into has prefix syntax and uses the
>same names for connectives
>as SCL. </p>
>
><p>For example, <i>imp(P(a),R(a))</i> would be an implication in
>traditional FOL, <i>Forall((x,y), P(x,y))</i> would be a quantified
>formula with two variables <i>x,y</i> quantified over.</p>
>
><p>It is a trivial matter to convert traditional FOL in this prefix syntax
>to another traditional FOL with an infix syntax, where the previous
>two examples could look like
><i>P(a) <tt>-></tt> R(a)</i>
>and
><i>Ax.Ay.P(x,y)</i>.</p>
>
><p>The following translation function <tt>T</tt>
>converts any SCL construction to "traditional" FOL
>syntax using the principles explained in this chapter:</p>
>
><p>
><ul>
> <li>
> If <i>c</i> is an SCL primitive, then
> <i></i><tt>T</tt><i>(c)</i> <tt>==></tt> <i>c</i>
> <li>
> Otherwise <tt>T</tt> is defined for each concrete numeric
> value of <i>n</i> in <i>en, Term_n, Atom_n,
>Formula_n</i> and <i>Sequence_n</i> as:
> <ul>
> <li>
> <i></i><tt>T</tt><i>(Term_n(e1,...,en))</i>
> <tt>==></tt>
> <i>Term_n(</i><tt>T</tt><i>(e1),...,</i><tt>T</tt><i>(en))</i>
> </li>
> <li>
> <i></i><tt>T</tt><i>(Atom_n(e1,...,en))</i>
> <tt>==></tt>
> <i>Atom_n(</i><tt>T</tt><i>(e1),...,</i><tt>T</tt><i>(en))</i>
> </li>
> <li>if <i>c</i> in <tt>T</tt><i>(c)</i>
> is an SCL formula <i>Formula_n(e1,...en)</i>, then either:
> <ul>
> <li>
> <p>if <i>e1</i> is an SCL connective primitive, then:</p>
> <p>
> <i></i><tt>T</tt><i>(Formula_n(e1,...,en))</i>
> <tt>==></tt>
> <i>e1(</i><tt>T</tt><i>(e2),...,</i><tt>T</tt><i>(en))</i>
> </p>
> </li>
> <li>
> <p>if <i>e1</i> is an SCL quantifier primitive, then:</p>
> <p>
> <i></i><tt>T</tt><i>(Formula_n(e1,...,en))</i>
> <tt>==></tt>
> <i>e1(e2,</i><tt>T</tt><i>(e3))</i>
> </p>
> </li>
> </ul>
> </li>
> <li>
> <i></i><tt>T</tt><i>(Sequence_n(eq,...,en))</i>
> <tt>==></tt>
>
><i>and(</i><tt>T</tt><i>(e1),and(</i><tt>T</tt><i>(e2),and(...,</i><tt>T</tt><i>(en))..)</i>
> </li>
> </ul>
></ul>
></p>
>
><p>The translation scheme introduces function symbols <i>Term_1,Term_2,...</i>
>and predicate symbols <i>Atom_1,Atom_2,...</i>
>into the traditional FOL formula
>created. In fact, the created formula contains <b>only</b> function symbols
>with the form <i>Term_i</i> and <b>only</b> predicate symbols with the form
><i>Atom_i</i> for various concrete numeric
>values of <i>i</i>.</p>
>
>
><h2><a name="modelstandalone">Standalone semantics of core SCL</a></h2>
>
><h2><a name="fullscl">Full SCL modules</a></h2>
>
><h3><a name="sclannot">SCL-ANNOT: annotations</a></h3>
>
><h3><a name="sclrole">SCL-ROLE: role symbols</a></h3>
>
><h3><a name="sclrestquant">SCL-RESTQUANT: restricted quantifiers</a></h3>
>
><h3><a name="scleq">SCL-EQ: equality</a></h3>
>
><h3><a name="sclint">SCL-INT: integers</a></h3>
>
><h3><a name="sclstring">SCL-STRING: strings</a></h3>
>
><h3><a name="scllist">SCL-LIST: lists</a></h3>
>
><h3><a name="sclseqvar">SCL-SEQVAR: sequence variables</a></h3>
>
><h2><a name="syntaxes">Concrete syntaxes</a></h2>
>
><h3><a name="sclprefix">SCL/PREFIX concrete syntax</a></h3>
>
><h3><a name="sclkif">SCL/KIF concrete syntax</a></h3>
>
><h3><a name="sclxml">SCL/XML concrete syntax</a></h3>
>
><h3><a name="scln3">SCL/N3 concrete syntax</a></h3>
>
><h2><a name="examples">Larger examples</a></h2>
>
><h2><a name="scltordf">Translation example: RDF translation to SCL</a></h2>
>
><h2><a name="acknowledgements">Acknowledgements</a></h2>
>
><h2><a name="glossary">Appendix A: Glossary</a></h2>
>
><h2><a name="usage">Appendix B: Notes about Usage</a></h2>
>
><h2><a name="references">Appendix C: References</a></h2>
><ul>
> <li><b>FOL</b>
> <ul>
> <li>
> <a href="http://plato.stanford.edu/entries/logic-classical/">
> http://plato.stanford.edu/entries/logic-classical/</a></li>
> <li>... we need a link to FOL presentation containing function symbols
> and terms: the plato link presents FOL
>without function symbols ...</li>
> <li>
> <a href="http://logic.philosophy.ox.ac.uk/main.htm">
> http://logic.philosophy.ox.ac.uk/main.htm</a></li>
> </ul></li>
>
> <li><b>KIF</b>
> <a href="http://logic.stanford.edu/kif/specification.html">
> http://logic.stanford.edu/kif/specification.html</a></li>
> <li><b>XML</b>
> <a href=" http://www.w3.org/XML/">
> http://www.w3.org/XML/</a></li>
> <li><b>N3</b>
> <a href="http://www.w3.org/DesignIssues/Notation3.html">
> http://www.w3.org/DesignIssues/Notation3.html</a></li>
>
>
></ul>
><h2><a name="changes">Appendix D: Changes From Previous Version</a></h2>
>
>The list of changes indicates the date of the publication of a new
>version, the name of the publisher, and the major differences from
>the previous version. Newer versions should occur at the top of the list.
>There are no version numbers.
>
><p>In the final specification this list will be reformatted and simplified:
>the current form is meant only for the specification as work in progress.
></p>
>
><ul>
>
><li>1 nov 2003, T.Tammet.
> <ul>
> <li>Few cosmetic modifications to the
>"Basic principles of SCL" chapter</li>
> <li>Role symbols added to contents, basic features and a list of empty
> chapters. See
> <a href="http://philebus.tamu.edu/pipermail/scl/2003-July/000307.html">
> this mail by P.Hayes</a></li>
> <li>Restricted quantifiers (example:
>(exists ((P ?X)) (R ?X))) module chapter
> is added to the list of chapters, contents, and a brief overview of
> the full SCL modules in the "Basic principles" chapter. Effectively, this
> means that the restricted quantifiers are moved out of the core SCL
> (to keep the core as free from syntactic sugar as possible) </li>
> <li>Moved the "Concrete syntaxes" chapter
><b>after</b> the "Full SCL" (modules)
> chapter. This should
> streamline the presentation: otherwise we would have to mention all the
> various syntaxes in the "modules" chapters. Now it is OK to only use
> the abstract syntax and the SCL/KIF syntax in these chapters.</li>
> <li>Replaced the "SCL/LISP" concrete syntax
>with "SCL/KIF" concrete syntax
> (chapter title in contents and the
>corresponding empty chapter). Mentioned
> this in the "Basic principles" chapter.</li>
> <li>Added the "Informal SCL/KIF concrete
>syntax for core SCL" chapter immediately
> after the "Abstract" syntax chapter, to
>allow bringing examples in a concrete
> syntax as early as possible. </li>
> <li>Added the "SCL/N3 concrete syntax" chapter to the list of concrete
> syntax chapters. This should be useful for people considering SCL from
> thr RDF(S) viewpoint. NB! The SCL/N3 is not the same as N3. On one hand,
> a large number of constructions in N3 is thrown out, while full SCL is
> covered. N3 is a suitable example syntax
>since N3 contains ordinary logical
> rules and variables in the syntax, differently from RDFS and OWL.
> </li>
> <li>Added some references to the reference
>list (initially, for convenience
> and for indicating a need to collect suitable references)</li>
> <li>Added an temporary version of the "SCL
>core abstract syntax" chapter.
> See editorial notes at the beginning of the chapter.</li>
> <li>Added an early version of the
>"Translation of core SCL to FOL: semantics
> via FOL" chapter. See editorial notes at
>the beginning of the chapter.</li>
>
> </ul>
> </li><li>30 oct 2003, T.Tammet. First version of the spec, based on earlier
> fragments and principles by all the members of the SCL group.</li>
>
>
></ul></li>
></ul>
>
>
></body></html>
></x-html>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32501 (850)291 0667 cell
phayes at ihmc.us http://www.ihmc.us/users/phayes
More information about the SCL
mailing list