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

From: Michael Kifer <kifer@cs.sunysb.edu>
Subject: Re: [RIF] Reaction to the proposal by Boley, Kifer et al 
Date: Wed, 03 May 2006 23:20:02 -0400

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

Do you really mean this, i.e., that there is essentially only one domain of
discourse?  Are there no possibilities of non-trivial identity, for example
between f(a) and f(b)?

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

Well, at least unless you have an infinite number of axioms.

> This is one reason why the most common
> semantics for default negation rely on infinite Herbrand models.
> 
> 	--michael  

It still would be useful to have a pointer to a full description of the
logic (or logics).

peter

Received on Thursday, 4 May 2006 10:39:17 UTC