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

From: Benjamin Grosof (bgrosof@MIT.EDU)
Date: 07/01/03

  • Next message: Peter F. Patel-Schneider: "belated (and not) regrets"
    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(?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
    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 or

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