[SCL] XML concrete syntax early internal draft

Tanel Tammet tammet at staff.ttu.ee
Tue Apr 29 10:02:47 CDT 2003


Hi,

First, I am sorry I have not been able to participate at
the last few telecons. Tried today, though, but either
no one was there or I picked wrong times to call.

Anyway, I have finished an early draft for the
XML syntax of SCL. It is NOT a draft of a publishable
document: it is a draft for our internal discussion.
Once it seems we agree on most (or critical) points,
I'll write a publishable draft.

Please have a look and find out some things which
could or should be improved.

The draft is attached as a plain text file.

PS: in order to make the XML spec complete we have
to invent a namespace URI sooner or later. Preferrably
an URI where we will hang the SCL documents.

PS: I was thinking about - possibly - writing a draft
for proof syntax in XML, once we get the language
draft ready. I have worked on the proof syntax before:
this is not something which can be made to satisfy
all parties. Rather, one could should aim to have a
sensible, yet relatively simple syntax which can be extended
heavily for different purposes.

Regards,
          Tanel Tammet

-------------- next part --------------
XML syntax for SCL level 1 
--------------------------
Internal draft
Tanel Tammet
29 april 2003


Introduction
------------

This draft contains a concrete suggestion for encoding
SCL in XML, presented with minimal details. Necessary
additions, explanations, examples, etc will be added after
the basic details have been agreed upon.

Approach (explanatory)
-----------------------

The approach used is a compromise between minimalism and
the ordinary ways to represent data in XML. In particular,
we attempt to encode some data in tag structures and some
data as arguments to tags.

The language should be easily extendable by users by:
- using connective and type names invented by the users
- using parameters invented by the users
- putting free-form XML into SCL terms

The language does not follow the example of RDF and OWL
in the sense that the arity of predicates is not restricted.
However, we envision that RDF and OWL structures can be
put into the SCL structures, using the proposed xmlterm tag.

The arity of associative connectives is not restricted.
The arity of non-associative connectives is restricted.


Example
-------

We start with an example. Consider the following list of 
three formulas (with no recognisable meaning):

exists x:r forall y . p(x,f(1,a)) & -m(y,10,"a string","<foo>an xml string</foo>").
exists x. p(x,1) => equal(x,1).
forall x. -p(x,x).

<scl:connective 
    xmlns:scl="http://scluripart"
    scl:name="and">
  <scl:quantifier scl:name="exists" scl:variable="x" scl:type="r" 
                  scl:comment="first formula">
    <scl:quantifier scl:name="forall" scl:variable="y">
        <scl:connective scl:name="and">
           <scl:predicate scl:name="p">
             <scl:term scl:name="x">
             <scl:term scl:name="f">
               <scl:term scl:name="1"/>
               <scl:term scl:name="a"/>
             </scl:term>  
           </scl:predicate> 
        </scl:connective>
        <scl:connective scl:name="not" 
                        scl:comment="second formula">
          <scl:predicate scl:name="m">
            <scl:term scl:name="y">
            <scl:term scl:name="10">
            <scl:term scl:name="a string">
            <scl:xmlterm>
              <foo>an xml string</foo>
            </scl:xmlterm>  
          </scl:predicate>  
        </scl:connective>                      
    </scl:quantifier>       
  </scl:quantifier>   
  <scl:quantifier scl:name="exists" scl:variable="x">
     <scl:connective scl:name="implies">
        <scl:predicate scl:name="p">
            <scl:term scl:name="x"/>
            <scl:term scl:name="1"/>
        </scl:predicate>  
        <scl:predicate scl:name="equal">
            <scl:term scl:name="x"/>
            <scl:term scl:name="1"/>
        </scl:predicate>        
     </scl:connective>                      
  </scl:quantifier>
  <scl:quantifier scl:name="forall" scl:variable="x" 
                  scl:comment="third formula">
     <scl:connective scl:name="not">
        <scl:predicate scl:name="p">
            <scl:term scl:name="x"/>
            <scl:term scl:name="x"/>
        </scl:predicate>          
     </scl:connective>                      
  </scl:quantifier>
</scl:connective> 
        
Principles of encoding
----------------------

SCL namespace defines the following tags:

- connective
- quantifier
- predicate
- term
- xmlterm (NB! may occur in arbitrary places in the SCL structure)

and the following parameters for tags:

- name (obligatory for all scl tags)
- variable (allowed and obligatory only for scl quantifier tags)
- type (allowed only for scl quantifier tags)
- comment (allowed for all scl tags)

SCL further defines the following name parameter 
value strings with predefined meanings (meaning
defined as such only if the value occurs in a suitable
SCL tag):

- exists  (meaning defined iff in quantifier tag)
- forall  (meaning defined iff in quantifier tag)
- and     (meaning defined iff in connective tag)
- or      (meaning defined iff in connective tag)
- xor     (meaning defined iff in connective tag) 
- implies (meaning defined iff in connective tag) 
- not     (meaning defined iff in connective tag)
- equivalent (meaning defined iff in connective tag)
- equal   (meaning defined iff in predicate tag)

 
What is not prohibited
----------------------- 

SCL does not prohibit using additional tags, parameters and parameter
values inside SCL text structures. 

SCL parsers (unless specially extended) should simply 
ignore all unknown tags, parameters and values.

Suggestions for extensions
--------------------------

Language users can easily create richer languages on top of 
SCL, using their own namespaces. Some of the suggested ways:

- using additional tag parameters
- using additional connective tag name parameter values
- using additional quantifier tag name parameter values
- using arbitrary XML inside the xmlterm tag

In particular, users can invent their own parameters to 
mark formulas as belonging to different parts of the knowledge
base (for example: axioms for arihtmetic, theory of lists, 
knowledge of a particular person, a query, etc).



More information about the Scl mailing list