comments invited: draft of axiomatization of explicit equality for LP rules language

• Previous message: Harold Boley: "Equality Hubs"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

Draft of explicit axiomatization of equality for RuleML / DAML Rules

by Benjamin Grosof

version V1 of 7/1/03

% (file housekeeping memo to Benjamin:  this file is axiomatization-1.txt,
%  excerpted from file equality/thoughts-1.txt)

Background:  see Joint Committee telecon discussion of 7/1/03, including
- Mike Dean's test cases
- Benj's notes from the telecon

Here's a pass at defining an axiomatization, within a declarative
(definite Horn) LP language itself,
of explicit equality.  Here, equality is
treated as essentially an ordinary predicate (rather than specially
within the model theory).
Let ee stand for the explicit equality predicate.

1. symmetry:

   ee(?y,?x) <- ee(?x,?y);

2. transitivity:

   ee(?x,?z) <- ee(?x,?y) and ee(?y,?z);

3. substitutivity for predicates:

Let P1,...,Pm be the predicates of the LP language.
Let the arity of Pi be ni, where ni >= 0.

For each Pi, i=1,...,m, and for each j=1,...,ni:

   Pi(?X1,...,?W,...,?Xni) <- ee(?Xj,?W) and Pi(?X1,...,?Xj,...,?Xni);

Actually, one can equivalently omit this if ni=0.

4. substitutivity for logical functions, i.e., constructors:

Let F1,...,Fk be the logical functions of the LP language.
Let the arity of Fi be ni, where ni >= 0.

For each Fi, i=1,...,k, and for each j=1,...,ni:

   ee(?Y,Fi(?X1,...,?W,...,?Xni))
          <- ee(?Xj,?W) and ee(?Y,Fi(?X1,...,?Xj,...,?Xni));

Actually, one can equivalently omit this if ni=0.


Issue/Q todo:  do we need to say anything else about equality other
than the above (1.)-(4.)?
- E.g., is there anything different about skolem functions?
- E.g., is there something that needs to be said about how unification
treats equality in corresponding proof theory (since the usual
definition of unification ignores equality other than syntactic
identicality)?

todo: Look at how FOL with equality has been formalized, including
unification in it.



________________________________________________________________________________________________
Prof. Benjamin Grosof
Web Technologies for E-Commerce, Business Policies, E-Contracting, Rules, 
XML, Agents, Semantic Web Services
MIT Sloan School of Management, Information Technology group
http://ebusiness.mit.edu/bgrosof or http://www.mit.edu/~bgrosof

• text/plain attachment: axiomatization-1.txt

• Next message: Peter F. Patel-Schneider: "belated (and not) regrets"
• Previous message: Harold Boley: "Equality Hubs"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.4 : 07/01/03 EST