Re: Notes on 7/20 BLD draft

Hassan Aït-Kaci wrote:
> 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.

*sigh*

I failed again to completely capture my proposal in that one 
paragraph, but I know I said it at some point - in addition to prenex 
syntax, the BLD would of course need additional constraints to stay in 
horn, such as (but not limited to) restricting existentially 
quantified variables from the head.  But for sure EVERY *first order* 
dialect can be expressed (with suitable restrictions for the dialect 
of course) in prenex.

I think it is just a cleaner syntax, but as I said I really don't feel 
that strongly about it....each time I reply to a message in this 
thread I hesitate even longer wondering if it is worth it....

I guess the thing that "bothers" me about the current syntax is the 
asymmetry of quantification, and this is what I'm trying to "fix". 
Logic has a certain beauty to it, you know.

-Chris


> 
> -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 
>>
>>
> 
> 

-- 
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 07:16:51 UTC