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

> > It is a standard result that unsatisfiability for clausual form in FOL is
> > the same as unsatisfiability in Herbrand models alone.
> > So, for clauses unsatisfiability is semi-decidable in both.
> > Therefore, entailment is also semi-decidable.
> > 
> > The real difference comes into play when existential quantifiers are taken
> > into account. If you use Herbrand domains with infinite supply of
> > function symbols of every arity, then again unsatsfiability is
> > semi-decidable because you can reduce things to clausal form again.
> > 
> > Note that the above web site talks about the standard Herbrand models,
> > which uses only the symbols that occur in the program itself (otherwise,
> > their undecidability proof that is based on Diophantine equations) breaks.
> > 
> > Note that in our proposal we talked about infinite Herbrand universes (which
> > are domains with infinite supply of every function symbol and constants).
> 
> OK, but then I'm still waiting for some definition of a logic based on
> "infinite Herbrand interpretations".

It has the same FOL syntax, but the language, L, contains an infinite # of
function symbols for every arity (0 and on). All interpretations are
Herbrand over that language.

The difference with the usual definition of Herbrand interpretation is that
in the usual one the Herbrand universe of a KB, K, is constructed out of
only the constants and function symbols that appear in K. In infinite
Herbrand models, the universe is constructed using all the function symbols
in the language L.

So, for example, the proof of undecidability on the web site pointed to by
Hasan won't work for infinite HMs because it relies on the fact that
successor (s) is the only function symbol.

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 for skolemization. This is one reason why the most common
semantics for default negation rely on infinite Herbrand models.


	--michael

Received on Thursday, 4 May 2006 03:23:40 UTC