# Herbrand Universe + Resolution

Posted by late_student
Announcements Last Post
SoC Curricula 09/30/2017 01:08PM
Demarcation or scoping of examinations and assessment 02/13/2017 07:59AM
School of Computing Short Learning Programmes 11/24/2014 08:37AM
Unisa contact information 07/28/2011 01:28PM
 Herbrand Universe + Resolution January 28, 2009 11:07AM Registered: 10 years ago Posts: 5 Rating: 0
Can anyone here explain how Question4, iii in the tut was arrived at? It almost seems arbitrary
Is the universe extracted from the clausal form or from the original ?
Why was iii a,b,c instead of f(a) ?

also

When looking at resolution and hoping to arrive at a []. Is it acceptable to arrive at [] early ? i.e. if i get there in 2 steps, do i need to continue or can i decide then that its not satisfiable because i was able to reach a [] ?
 Re: Herbrand Universe + Resolution January 28, 2009 11:36PM Registered: 13 years ago Posts: 1,682 Rating: 0
From my understanding (and I may be wrong)

(1) The Herbrand Universe is a list of the constants and the functions (with all possible elements being possible assigments to the function). Since iii has no functions you just list the three constants.

(2) yes; the moment you have the [] you've won.

```
,= ,-_-. =.
((_/)o o(\_))
`-'(. .)`-'
\_/```
http://ilanpillemer.com
Entia non sunt multiplicanda praeter necessitatem
 Re: Herbrand Universe + Resolution January 29, 2009 12:35AM Registered: 10 years ago Posts: 5 Rating: 0
Thanks muchly..
Sorry, only registered users may post in this forum.