Welcome! Log In Create A New Profile


Herbrand Universe + Resolution

Posted by late_student 
Announcements Last Post
Announcement : Programming Students at UNISA School of Computing 06/19/2019 02:01PM
Announcement SoC Curricula 09/30/2017 01:08PM
Announcement Demarcation or scoping of examinations and assessment 02/13/2017 07:59AM
Announcement School of Computing Short Learning Programmes 11/24/2014 08:37AM
Announcement Unisa contact information 07/28/2011 01:28PM
Herbrand Universe + Resolution
January 28, 2009 11:07AM
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) ?


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 [] ?
avatar Re: Herbrand Universe + Resolution
January 28, 2009 11:36PM
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(\_))
  `-'(. .)`-'
Entia non sunt multiplicanda praeter necessitatem
Re: Herbrand Universe + Resolution
January 29, 2009 12:35AM
Thanks muchly..
Sorry, only registered users may post in this forum.

Click here to login