- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Tue, 05 Sep 2006 07:01:48 -0400
- To: Chris Welty <cawelty@frontiernet.net>
- Cc: public-rif-wg@w3.org
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