- From: Chris Welty <cawelty@gmail.com>
- Date: Tue, 24 Jul 2007 17:15:58 -0700
- To: Michael Kifer <kifer@cs.sunysb.edu>
- CC: "Boley, Harold" <Harold.Boley@nrc-cnrc.gc.ca>, "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>
Michael Kifer wrote: >> >> Michael Kifer wrote: >>>>>> * It seems to me a cleaner syntax is to remove existentials from >>>>>> conditions and unify all quantifiers outside the rule (as with >>>>>> universal now), and add a restriction in horn that existentially >>>>>> quantified vars cannot appear in the conclusion. >>>>> The RIF Basic Condition Language is meant to be reusable also >>>>> (in PR and) outside the context of any rule, stand-alone (e.g. >>>>> for queries and integrity checking), where existentials cannot >>>>> be rewritten as universals in the Example 3b.->3a. manner. >>>> Oh, you misunderstood - I did not mean eliminate existentials from the >>>> syntax entirely, I meant move them outside conditions into some sort >>>> of wrapper or context (like, rules). This would make, at least, the >>>> rule syntax cleaner. >>> Unless I misunderstood you, what you are proposing is not sound in FOL: >>> >>> Exists X foo <- bar(X) >>> >>> is not the same as >>> >>> foo <- Exists X bar(X). >> As you know full well this kind of mapping is easily fixed by >> rewriting the variable names. >> >> -Chris > > No. foo <- Exists X bar(X) is foo \/ not Exists X bar(X) > which is foo \/ forall X not bar(X) > which is forall X foo <- bar(X) (after possible variable renamings). > This is different from Exists X foo <- bar(X). Hmmmm. We seem to be agreeing furiously. Sorry if I'm being too opaque and imprecise - it comes from terseness. I'm merely proposing prenix normal form (for rules). Any first order sentence can be written in prenex. My only reason for this proposal is that it seems to be a cleaner and easier to process syntax. Do you agree? I don't feel that strongly about it, but each time I see the abstract syntax it reminds me that prenix would be simpler. -Chris > > So, your proposal amounts to removing existentials from the rules completely. > This is how we understood it and Harold pointed out that there was > a decision to keep the existentials in the rule body. > Then you said that you did not mean to delete the existentials, but to move > them to the outside of the rule. I pointed out that this is unsound, and > your remark about fixing this by renaming is wrong, as shown above. > > Did I misunderstand u again? > > > --michael > -- Dr. Christopher A. Welty IBM Watson Research Center +1.914.784.7055 19 Skyline Dr. cawelty@gmail.com Hawthorne, NY 10532 http://www.research.ibm.com/people/w/welty
Received on Wednesday, 25 July 2007 00:16:11 UTC