- From: Uli Sattler <Ulrike.Sattler@manchester.ac.uk>
- Date: Thu, 4 May 2006 12:22:26 +0100
- To: RIF WG <public-rif-wg@w3.org>
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