[SCL] Re: The second draft for XML syntax for CL

[geoff at cs.miami.edu]

Hi,

Comments about Tanle's comments about Murray's comments ...

> > But what about extensions? What if someone wants meet(i,j)? How
> > will a processor know its correct arity?
> 
> In the tivial sense the arity of predicates and functions is arbitrary:
> it is only important that the arity of "meet" is the same in
> all its occurrences in the whole formula. This is easy to check
> after or while parsing.

With the arity specified you can then immediately check if the
creator (man or machine) has provided the correct number of
arguements. Also, maybe to your frustration, many believe that
the arity of a predicate/functor is part of its identity, and will
happily write logic where the same symbol is used with different
arities, and worse, as both a predicate and a funtor. Do you
disallow that (hence making the syntax unusable for those situations)?
 
> It is very very important that people can extend the core language.
> 
> Look at the actual, practical necessities in the TPTP library
> of thousands of FOL problems. The TPTP author/maintainer Geoff
> will tell you any day that it is absolutely necessary to add
> various metainformation to formulas.

I confirm that, and indeed, my new TSTP syntax explicitly provides
place for arbitary annotations. The constraint is that the annotations
must be formated as terms, so I can use the same parsing tools to
extract structure from the annotations. See the <useful info> fields
in http://www.cs.miami.edu/~tptp/TSTP/TSTPBNF.txt .
 
> >>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).
> > 
> > Are there any rules for this, or do we expect to receive an SCL
> > document and have to figure out what it means by hand? Will 
> > non-standard SCL documents be labeled differently than ones that
> > conform to the standard?

What I have done is identified where these can occur, which then allows
them to be ignored safely. They are not part of the principle information
being conveyed.
 
Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264