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

With equality the domain of interpretation is a set of equivalence classes
over the Herbrand universe.  Herbrand universe != Herbrand domain in case
there is equality.  This is all standard stuff in Logic Programming.
http://citeseer.ist.psu.edu/context/6262/0
Also see the classical Chang & Lee's book:

@book{ chang-lee,
author = "C.L. Chang and R.C.T. Lee",
title = "Symbolic Logic and Mechanical Theorem Proving",
publisher = "Academic Press",
year = 1973
}

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

No. Unless your set of axioms uses up all but a finite set of symbols of
some arity.

Received on Thursday, 4 May 2006 15:10:11 UTC