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.