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 17:03:23 -0400

> 
> > 
> > From: Hassan Aït-Kaci <hak@ilog.com>
> > Subject: Re: [RIF] Reaction to the proposal by Boley, Kifer et al
> > Date: Wed, 03 May 2006 10:15:48 -0700
> > 
> > > Peter F. Patel-Schneider wrote:
> > > 
> > > > From: Francois Bry <bry@ifi.lmu.de>
> > > > 
> > > >>Peter F. Patel-Schneider wrote:
> > > >>
> > > >>>>This is based on a known logic: infinite Herbrand interpretations.
> > > >>>
> > > >>>Reference, please.
> > > >>
> > > >>I could maybe help in giving reference if I would understand what you
> > > >>are asking for.
> > > > 
> > > > A reference to logics based on infinite Herbrand intepretations that shows
> > > > how they relate to standard first-order logics.
> > > 
> > > http://logic.stanford.edu/~thinrich/herbrand/html/index.html
> > 
> > Thanks, this is what I was asking for.
> > 
> > > Hassan Aït-Kaci
> > 
> > Now that that is cleared up ...
> > 
> > From that page:
> > 
> > 	With functions, entailment is not semi-decidable and satisfiability
> > 	is not semi-decidable.
> > 
> > I wonder, then, what is the relationship between this logic and standard
> > FOL.
> > 
> > peter
> 
> It is true that satisfiability is not semi-decidable, but it is not
> semi-decidable in FOL also.

But entailment is semi-decidable in FOL.

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

> The answer-set and the well-founded semantics are based on such models.
> 
> I am not sure is inference under infinite H models and under general models
> coincide for FOL syntax.  
> 
> 	--michael  

peter

Received on Thursday, 4 May 2006 02:55:32 UTC