Re: FO semantics for condition language (Action 84)

This proposal is nothing more than a simple structural reorganization of 
Peter's proposal to emphasize the correspondence to RIF phases.


   A Proposal for a First-Order Semantics for the Condition Language

I propose that the semantics for the condition language be based (solely)
on a standard first-order semantics.

The syntax for the core (Phase I) condition language (without negation) is:

 Data     ::= value
 Ind      ::= object
 Var      ::= '?' name
 TERM     ::= Data | Ind | Var | Expr
 Expr     ::= Fun '(' TERM* ')'
 Atom     ::= Rel '(' TERM* ')' | TERM '=' TERM
 LITFORM  ::= Atom
 QUANTIF  ::= 'Exists' Var+ '(' CONDIT ')'
 CONJ     ::= 'And' '(' CONDIT* ')'
 DISJ     ::= 'Or' '(' CONDIT* ')'
 CONDIT   ::= LITFORM | QUANTIF | CONJ | DISJ

The semantics for this condition language are essentially compatible with
the standard semantics for first-order logic without negation.

More formally:


Let D be a non-empty set (of domain elements), divided into DD (data) 
and DI (non-data).

Let Data be the set of syntax elements recognized by the Data / value 
production,
   Ind be the set of syntax elements recognized by the Ind / object 
production,
   Var be the set of syntax elements recognized by the Var / ?name 
production,
   Fun be the set of syntax elements recognized by the Fun production,
   Rel be the set of syntax elements recognized by the Rel production.

An interpretation I is then five mappings
   ID from Data to elements of DD
   II from Ind to elements of DI
   IV from Var to elements of D
   IF from Fun to functions from D* into D
   IR from Rel to subsets of D*

Interpretations are extended to terms as follows:
   I(v) = ID(v)     for v a value
   I(o) = II(o)    for o an object
   I(?v) = IV(?v)    for v a variable
   I(f(t1,...,tn)) = I(f)(I(t1),...,I(tn))

An interpretation satisfies a piece of syntax as follows
   I satisfies R(t1,...,tn)    iff    < I(t1),...,I(tn) > is in IR(R)
   I satisfies t1  = t2        iff    I(t1) = I(t2)
   I satisfies And(c1,...,cn)    iff    I satisfies ci for each 1<=i<=n
   I satisfies Or(c1,...,cn)    iff    I satisfies ci for some 1<=i<=n
   I satisfies Exists v1 ... vn c    iff    there is some I* that
                       agrees with I except for
                       the mappings of v1 ... vn
                       and I* satisfies c       
Built-ins are handled by requiring that interpretations have to be
compatible with the intended interpretation of the built-in Fun or Rel.
This can be used to handle ontologies as well.


Note 1:  The condition language may need to be tweaked somewhat as it
currently divides constants between data and individuals, but does not so
divide variables or functions.

Note 2:  This treatment pushes variables into the interpretation itself,
which is not the most common treatment, but works just the same.  If
someone cares, the treatment can easily be changed to the other way.

EXTENSIONS

The syntax for the "negation" extension to the core condition language 
is the core syntax with the addition that:

  LITFORM ::= Atom | 'Neg' Atom | 'Naf' Atom | 'Naf' 'Neg' Atom

This syntactic extension should be more-or-less uniform across different 
semantics; it is expected that for some RIF dialects, no difference will 
be made between "neg" and "naf".  In particular, the FO semantics for 
this condition language are essentially compatible with the standard 
semantics for first-order logic. It is the core semantics with the 
addition that:

   I satisfies Neg a        iff    I does not satisfy a
   I satisfies Naf a        iff    I does not satisfy a
   I satisfies Naf Neg a        iff    I satisfies a

Received on Friday, 1 September 2006 13:04:10 UTC