[SCL] CL syntax and Semantics

[Chris Menzel]

On Tue, Apr 08, 2003 at 04:03:32PM -0400, Pat Hayes wrote:
> Actions:
> Pat to complete draft of initial document (continued)
> John to write sketch of CG generalized concrete syntax
> Chris to adapt CL abstract syntax to the SCL core case

I have put a modification of the original CL document online at
http://cl.tamu.edu/docs/cl-fol.html.  This was banged out pretty quickly
so there are surely errors and other infelicities.  Also, while I have
tried to soften the tone a bit and make things a bit less mathy, and
have tried to give some illustrative examples, I have not gone to great
lengths, as the point was to get the content right; Pat is much better
than I am at that sort of feelgood stuff anyway. ;-)

Features of the language (all revisable):

* Seq vars clobbered
* No wild west syntax -- there are predicate constants, function symbols, 
  individual variables, and individual constants.  Predicates constants and 
  function symbols cannot occur as arguments to other predicates.
* Predicate constants and function symbols are variably polyadic; they
  have no fixed adicity.  NB: This is not an original idea -- Richard
  Grandy worked out a logic for such predicates many years ago. The 
  semantics is not appreciably different from ordinary first-order
  semantics.
* Currently, restricted quantification is allowed only with predicate
  constants, as both the syntax and semantics are complicated
  significantly if general conditions are allowed for the restrictions.
  Frankly, I see no point in allowing more complex restrictions (except
  *perhaps* simple boolean operations on predicates), as there then
  becomes no real advantage over the unrestricted counterparts of such
  formulas.

Comments encouraged. 

-chris