Re: FO semantics for condition language (Action 84)

It has been remarked already by 3 or 4 people that this proposal removes
the most useful type of negation that is employed in current rule-based
systems -- negation as failure.

And adding Naf to the language only in order to treat it as classical
negation in the semantics makes no sense whatsoever. At least, not to me.


	--michael  


> 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 Tuesday, 5 September 2006 11:05:00 UTC