- From: Peter F. Patel-Schneider <pfps@inf.unibz.it>
- Date: Wed, 03 May 2006 22:54:57 -0400 (EDT)
- To: kifer@cs.sunysb.edu
- Cc: hak@ilog.com, public-rif-wg@w3.org
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