[SCL] The second draft for XML syntax for CL
Tanel Tammet
tammet at staff.ttu.ee
Sun May 11 07:26:24 CDT 2003
Hi,
Attached please find the second version of the
SCL-in-XML draft.
This letter is sent to both the SCL list and
additionally to people not on the SCL list,
whi have helped with ideas and suggestions
about SCL-in-XML.
The main changes in the draft are:
- a TEMPORARY discussion part where I have
collected the discussion items. Each
item is commented, some ideas are introduced
as changes to the draft proper.
- referencing mechanism and a formula tag.
As always, please send new feedback.
NB! We need a draft of the SCL abstract syntax and
a draft of the SCL human-readable syntax.
IMHO further work on the SCL-in-XML draft is inefficient
until we get at least these two drafts.
For example, it is too early for nice formatting,
extensive references, a better example, DTD, etc.
Most likely the SCL-in-XML draft has to be
modified after these two more important
drafts appear.
It also appears that we may need a separate SCL-for-RDF draft.
I'll try to think how this language could look
like. Would be very useful if people having
extensively worked with RDF and OWL would come
up with some concrete suggestions and we could have
an initial discussion about the SCL-for-RDF language.
Pat has already expressed several ideas about this.
Regards,
Tanel Tammet
-------------- next part --------------
XML syntax for SCL level 1
--------------------------
SCL workgroup internal draft: second version
Tanel Tammet
11 May 2003
based on:
- the earlier draft from: 29 april 2003
- ideas, feedback and discussion after first draft with:
Geoff Sutcliffe, Murray Altheim, Pat Hayes, Dan Connolly
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.
Changes and motivations for these after the first draft
-------------------------------------------------------
This small chapter summarises the main feedback items
after version 1 of the draft. Each item is briefly commented upon
and it is indicated whether the current draft contains
a corresponding change and why.
The current chapter should NOT be a part of the spec:
it is here only for discussion purposes.
- Pat: XML is ugly, verbose, unreadable, hardly useful.
Comments by Tanel:
- we need alternative concrete syntaxes except
XML, geared towards human readability. However, once we want a
concrete XML syntax as well, we cannot escape the obvious
consequences there. Just have live with XML if we want to use it.
- the real point is the lack of need for extra parsers. We can
always assume that XML-represented logic can be parsed by any standard
XML parser, no need for additional implementation work to parse
a new syntax. Hence we should NOT attempt to put less-verbose-syntax
into XML documents: people would need an ADDITIONAL parser in such
cases, making their life significantly harder.
- Pat: We need to take seriously the potential need to interact
with the RDF style of using XML.
Comment by Tanel: we need an alternative concrete syntax for
combining logic in SCL with RDF. This document does not target
compatibility with RDF. Important issue, but has to be done differently.
Why differently? Because RDF is a straightjacket for ordinary
logic: in case we create an RDF-compatible syntax for SCL
(and we should do this!) it would be very hard to use this
syntax for "ordinary" logic.
- Geoff: XML is ugly, verbose, unreadable, hardly useful.
Comment by Tanel: see above.
- Geoff: need to encode annotations, e.g., names, type, etc, as in the
TPTP. Suggests to define a wrapper around the logic
formulae, and allow the annotations to be tag arguments or inner tag
structures. The TSTP annotation structure, which was designed to be very
flexible, may be a useful starting point (or ending point!).
Comment by Tanel:
- strictly speaking, we need no wrappers, since one can simply put
extra tag arguments with arbitrary string values into every tag.
All the annotations can and should be there.
- However, it may be convenient to have a top-level wrapper providing
an intuitive location for these annotation tags. Murray has introduced
a <formula> tag.
Change in version 2 of the draft: <formula> tag introduced.
Non-obligatory to use (this might change later).
- Geoff: allowing or requiring an arity value, e.g.,
<scl:connective scl:name="and" scl:arity=2>
That will make parsing and error reporting more robust.
Comment by Tanel: superfluous. Required arity or the lack
of it is pre-defined for each connective.
- Geoff: for quantified formulae the variable should be written outside
as a <scl:term/>.
Comment by Tanel: superfluous. In our minimalist approach
each term in the abstract syntax is converted to one tag in the
XML representation. We try to minimize the nr of tags, to keep
the structure simpler and flatter. Extra tags complicate the
structure. Hence keeping variable-as-an-argument-of-quantifier-tag
approach.
- Geoff: unique existence is something useful, the generalized form which the
TPTP will support is
? [1:X,2:Y] : p(X,Y)
meaning there are exactly one X and two Ys such that p(X,Y).
Comment by Tanel: no clear need to introduce this into minimal core
(we want to keep the core minimal!). Could be introduced in extensions.
Easy to give an extra parameter to quantifier tag, like this:
<quantifier name="exists" variable="x" count="2">
indicating that we say that there are exactly TWO instances.
However, bringing this into core creates unnecessary complications.
Let us see whether it will be in the SCL core - if yes, we can put
it into the XML concrete syntax.
- Murray: introduce <formula> tag
Comment by Tanel: see above: introduced in this version.
- Murray: shorten some, but no all, tag names,
for example <quant> instead of <quantifier>
Comment by Tanel: confusing to have some tag names as full
names in English, some as shortened. Better to keep full
names consistently. Since XML is very verbose anyway,
micro-optimisations such as shortening the tag names are useless.
- Murray: use XLINK namespace to refer to parts of other docs
Comment by Tanel: unclear why we need to to make other namespaces
obligatory. Rather, let us introduce a parameter href (as
xlink:href or just href in html) for referencing. This is subject
to discussion.
- Murray: introduce <doc> tag for arbitrary doc strings
Comment by Tanel: unnecessary, since we have a "comment" parameter
for free-form documentation strings. As said before, we do not
want to complicate the term structure by additional tags not
correspoding to SCL abstract syntax term elements. This
might change in case SCL abstract appears and demonstrates
that the mapping to XML term-as-tag would be useful.
- Murray: inroduce <type> tag to indicate the type of a variable
Comment by Tanel: this would open up a possibility to give
complex types attached to variables. The current proposal
of using "type" parameter only allows predicate names to
be used as types, simplifying the type usage. As said before,
we want to avoid new tags and complexities in structure.
- Murray: introduce reference tags, for example, <connRef>,
<quantRef>, etc
Comment by Tanel: MANY such tags are either superfluous or open
up a possibility for complex reference information.
One is enough. This has the advantage of having simple
"replacement" semantics, which can be seen as a separate layer.
Change in version 2 of the draft: "include" tag and "href" parameter
for this tag introduced. Semantics: replace the "include" tag with
href inside with a text referenced. Example:
<conn name="and">
<pred name="p">
<term name="1>
<include href="someuri1">
</pred>
<include href="someuri2">
</conn>
Any include tag (and no other tags) must contain href parameter.
Any include tag has to be replaced by the text referenced by href.
Change in version 2 of the draft: "id" parameter is introduced.
Any tag may contain "id".
NB! Observe we could use XLINK namespace instead of putting these
into SCL-in-XML namespace. In the current draft we DO NOT use XLINK
namespace, just to simplify matters. This may be changed.
- Dan: about Murray's reference tags like <termRef> etc:
not sure he groks termRef. Otherwise, it looks pretty straightforward.
Comment by Tanel: see above.
Summary of changes in the version 2 of the draft:
- some trivial errors (ending / forgotten at some places) corrected.
- formula tag introduced.
- include tag and the href parameter for this tag introduced.
- id parameter introduced.
- example modified to demonstrate the usage of "formula", "include"
"href" and "id".
(as said, "include" and "id" could be taken from other namespaces,
if we so wish: has to be discussed).
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.
The language contains a trivial mechanism for referencing
other texts and naming terms and formulas.
Example
-------
We start with an example. The example shows:
- formula representation in the proposed XML language
- references to other texts in the proposed XML language
Consider the following list of
three formulas (with no recognisable meaning) plus
a reference to an external file, plus a fourth formula
containing references to terms from another file.
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).
include formula at "someuri#foo"
r(include term at "someuri#bar", include term at "someuri#bar").
In addition, consider a DIFFERENT TEXT with an URI "someuri",
containing a formula identified as "foo" containing a term 1 identified as "bar":
forall x. -r(x,1).
We will have our first, main formula represented as the following text:
<scl:formula xmlns:scl="http://scluripart"
scl:comment="A meaningless example. Observe that the
formula tag is non-obligatory, bu provides a nice place
to add arbitrary annotations as parameters">
<scl:connective 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:include scl:href="someuri#foo">
<scl:predicate scl:name="r">
<scl:include scl:href="someuri#bar"/>
<scl:include scl:href="someuri#bar"/>
</scl:predicate>
</scl:connective>
</scl:formula>
And we will have another file with URI "someuri"
containing the referenced axiom(s) and term(s):
<scl:formula xmlns:scl="http://scluripart"
scl:comment="Axioms and terms to be included by other files,
observe that id is used as a parameter"
scl:id="foo">
<scl:quantifier scl:name="forall" scl:variable="x">
<scl:predicate scl:name="r">
<scl:term scl:name="x"/>
<scl:term scl:name="1"
scl:id="bar"/>
<scl:term/>
<scl:quantifier/>
<scl:formula/>
NB! Observe that the second (included) file need not be in the SCL-in-XML
language. We could, if we so wish, use such a file:
- - - - - - - -
<h1>Just a header in html</h1>
Now comes a formula part not visible in html browsers,
see the id parameter and include usage:
<scl:quantifier scl:name="forall" scl:variable="x"
scl:id="foo">
<scl:predicate scl:name="r">
<scl:term scl:name="x"/>
<scl:include scl:href="#bar">
<scl:term/>
<scl:quantifier/>
And here is the included term, also not visible in html browsers:
<scl:term scl:name="1"
scl:id="bar"/>
End of file.
- - - - - - -
Principles of encoding
----------------------
SCL namespace defines the following tags:
- formula
- connective
- quantifier
- predicate
- term
- xmlterm (NB! may occur in arbitrary places in the SCL structure)
- include (NB! is replaced by referenced text)
and the following parameters for tags:
- name (obligatory for all scl tags, except include)
- variable (allowed and obligatory only for scl quantifier tags)
- type (allowed only for scl quantifier tags)
- comment (allowed for all scl tags)
- href (allowed and obligatory only in the include tag)
- id (may be used in any tag, except include tag)
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