[SCL] Continuation

[Tanel Tammet]

Hi,

Since the first week of the new semester has passed, how
about restarting the SCL work? I hope there is still interest
after the almost-inevtiable break during summer.

I'll give a short overview of how I have personally
perceived the situation at the beginning of summer:

- Chris had written and rewritten etc a nice HTML paper
   about the semantics of basic SCL, in a self-contained manner.

- What was missing in the semantics paper (ie we had discussions
   about that):
   - integers and integer operators
   - metainformation (ie comments with no semantics)

- I was concerned with the relation of  SCL to standard FOL
   and insisted on witing down clear translation rules from
   SCL abstract syntax to standard FOL and vice versa.  

   This never really materialised, since:

    -  there was no clear consensus whether we should
       translate SCL atom P(a,b) as holds(P,a,b) in SFOL
       or not. I'd say, there was ALMOST a consensus,
       but with some doubts expressed now and then.
       In particular, Pat asked a number of FOL prover
      hackers about this translation, with the result that
      it seemed to be OK for everybody who answered.

    -  we did not reach a  consensus about the treatment
       of equality. My view is that we need two different equality
        predicates in the SFOL translation of SCL formulas,
        and I wrote several detailed proposals for that.
        These were not accepted as being OK, since
        Pat and Chris hoped to avoid two equalities.
        However, nobody ever came up with an SCL<=>SFOL
        translation schema where we'd have just one equality
        predicate and still avoid problems with Horrocks formulas.

- Additionally, Pat had always insisted on having varyadic
   quantifiers/predicates. As far as I remember, the
   semantics of these was never quite clearly written
   down in the SCL context (at least, the SCL<=>SFOL
   translation for these was not written down).

- At some point we did put effort into designing the concrete
  syntax of SCL in XML. This was later put on hold,
  until the semantics and abstract syntax of SCL become
  crystal clear.

IMHO the first step in moving forward would be to fix the
SCL <=> SFOL translation schema. There is nothing
to invent there, just to reach a consensus and write it
down.

If we manage to do that, then we need to proceed
to integers and comment strings. Put these into
syntax, describe semantics (also in SFOL sense).

The next step should be the varyadic variables,
if we still decide to keep these.

Regards,
         Tanel Tammet