- From: Hassan Aït-Kaci <hak@ilog.com>
- Date: Tue, 24 Jul 2007 17:29:40 -0700
- To: Chris Welty <cawelty@gmail.com>
- CC: Michael Kifer <kifer@cs.sunysb.edu>, "Boley, Harold" <Harold.Boley@nrc-cnrc.gc.ca>, "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>
Chris, Prenex form is a normal form for FOL, butnot for Horn logic. In other words, the prenex form of a Horn sentence may be non-Horn. Existentials in the condition part (the 'body' of a clause) are universals in hiding due to the 'not' lurking there (a <- b = a \/ not b). In fact, existentials in the body are allowed in (non-Horn) logic programming languages - e.g., based on Hereditary Harrop Formulae -or H2Fs). They are conveniently used programmatically for hiding local variables. The same for local implications (used for hypothetical reasoning) - also possible in H2F programming - e.g., lambdaProlog). Conclusion: your proposal re using prenex only will work for pure Horn languages, but not for other FOL dialects. This is what Michael tried to explain - I think. -hak Chris Welty wrote: > > > 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 > > -- Hassan Aït-Kaci * ILOG, Inc. - Product Division R&D http://koala.ilog.fr/wiki/bin/view/Main/HassanAitKaci
Received on Wednesday, 25 July 2007 00:32:07 UTC