 | This article is rated Stub-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
Unclear
editI'm having some trouble understanding the article. Its states:
- Moreover, Herbrand's theorem states that if S is unsatisfiable then there is a finite unsatisfiable set of ground instances from the Herbrand universe defined by S.
I don't understand how a set of ground instances can be "unsatisfiable". Perhaps the intended meaning is this:
- Moreover, Herbrand's theorem states that if S is unsatisfiable then there is a Herbrand interpretation with finite set of ground instances (from the Herbrand universe defined by S), and a finite set of predicates (from the Herbrand base of S) that are unsatisfiable?
Or am I crazy? I have only the vaguest grasp of the subject matter of this article; it could benefit from an example or two. linas (talk) 16:43, 9 April 2008 (UTC)
As to me, I do not understand this: "every function symbol is interpreted as the function that applies it" --Cokaban (talk) 22:55, 6 June 2008 (UTC)