Talk:Herbrand universe

From Wikipedia, the free encyclopedia

I can't tell the difference between a term algebra, and a Herbrand universe. These seem to be the same thing; maybe "term algebra" is more general, because it does not assume that the terms are first-order logic constructs?? Can someone clarify? linas (talk) 15:53, 9 April 2008 (UTC)

Err, maybe I've got it .. a Herbrand universe cannot contain any free variables, by definition. A term algebra does not even raise the issue of free variables, and so one can define a term algebra to consist of a set of constants, variables, and other terms. linas (talk) 15:57, 9 April 2008 (UTC)

[edit] Finiteness of a Herbrand Universe

Is it true that if the vocabulary contains at least one function symbol which has arity greater than zero and at least one constant symbol, then the Herbrand Universe of the Vocabulary is infinite?

Let g/1 be a unary function symbol, and c a constant -- one can also say a nullary function symbol. Then one could construct the ground terms g(c), g(g(c)), g(g(g(c))) ... i.e. infinitely many terms within the Herbrand Universe, correct? We could add this to the article. —Preceding unsigned comment added by 141.84.23.241 (talk) 09:50, 18 April 2008 (UTC)

Yes, that is correct. The Herbrand universe is only finite if all function symbols are constants. The sub-language of clausal logic with this property is decidable (but the decision problem is NEXPTIME-complete, if I remember correctly). --Stephan Schulz (talk) 09:57, 18 April 2008 (UTC)