- From: Peter F. Patel-Schneider <pfps@inf.unibz.it>
- Date: Thu, 04 May 2006 06:39:01 -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 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