Created on March 6, 2013, 4:28 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.
Resolution itself has certain Properties. One of them is the Completeness of Refutation
, which means if a Resolution is applied to a set of Clauses that contains a Contradiction, then there always exists a finite number of Resolution Steps to detect this Contradiction, but the problem is that the number that is required or needed to find the Resolution might be pretty high, so it is not a efficient method. On the other site Resolution of First Order Logic is undecidable, which means if one has a Set of Clauses and there is no Contradiction in it, then it is not guaranteed that this method will ever end. So one will until infinity combine Clauses with other Clauses and one will never find a Contradiction, i.e. in Resolution Step the empty Clause. Therefore Resolution for First Order Logic is undecidable. But on the other hand, for working with this in practice, whenever there is a Contradiction, one is able to proof it.
Comment on This Data Unit