Properties of FOL Resolution

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.

  • Completeness of Refutation
    • If Resolution is applied to a contradictory set of Clauses, then there exists a finite number of resolution steps to detect the contradiction.
    • The number n of necessary steps can be very large (not efficient)
  • Resolution in FOL is undecidable
    • If the set of Clauses is not contradictory, then the Termination of the Resolution is not guaranteed.

Tags: completness, solution, decidable
Categories: Concept
Parent: Resolution of First Order Logic

Update entry (Admin) | See changes

Comment on This Data Unit