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

> 
> 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>
> > > Subject: Re: [RIF] Reaction to the proposal by Boley, Kifer et al
> > > Date: Wed, 03 May 2006 14:21:28 +0200
> > > 
> > > 
> > >>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.

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

Received on Wednesday, 3 May 2006 21:04:21 UTC