- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Tue, 29 Aug 2006 12:31:17 -0400
- To: "Peter F. Patel-Schneider" <pfps@inf.unibz.it>
- Cc: public-rif-wg@w3.org
This is indeed an FOL. And it treats Naf as classical negation. Many in this group believe that negation as failure is an absolute must. So, I don't quite see the point. --michael > This proposal is nothing more than a simple modification to standard > first-order semantics to account for the syntax of the condition language. > > > > 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 condition language (with 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 > LITFORM ::= Atom | 'Neg' Atom | 'Naf' Atom | 'Naf' 'Neg' Atom > > The semantics for this condition language are essentially compatible with > the standard semantics for first-order logic. > > 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 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 > 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. > > >
Received on Tuesday, 29 August 2006 16:31:39 UTC