Re: [RIF] Reaction to the proposal by Boley, Kifer et al

On 4 May 2006, at 12:22, Francois Bry wrote:

>
>
>>>
>>> The idiosyncrasies of the logic over the usual Herbrand models  
>>> arise due to
>>> the fact that you can't always skolemize (you may not have enough  
>>> function
>>> symbols for that). But in infinite Herbrand models you always  
>>> have enough
>>> functions for skolemization.
>>>
>>
>> Well, at least unless you have an infinite number of axioms.
>>
>>
> Another formalization, which might be as well acceptable for RIF,  
> is as
> follows.
>
> Considering a finite set of formulas (or rules) expressed in a finite
> language, these formulas are first Skolemized what adds to the  
> language
> a finite number of function symbols. Then the Herbrand model is
> considered with its universe (= domain) being deiined as usual from  
> the
> finite language.

just to be clear that I understand you correctly: the signature is  
finite, yet there are infinitely many terms and infinitely many  
formulae...and the Herbrand universe is infinite in the presence of  
at least one function symbol?!

Cheers, Uli

>
> This way, the language is finitre and there is no need for an infinite
> number of axioms.
>
> Francois
>

Received on Thursday, 4 May 2006 11:25:39 UTC