Resolution in Predicate Logic

Resolution is a widely used inference rule in Predicate Logic (including FOPL) for proving the validity or satisfiability of a set of formulas. It is a proof technique that operates by resolving or combining clauses to derive new clauses until a contradiction is reached or no further resolutions are possible.

The resolution rule in Predicate Logic is an extension of the resolution rule in Propositional Logic. It incorporates the concepts of quantifiers, predicates, and variables. The resolution rule for Predicate Logic is as follows:

1. Standardize Variables: Before applying resolution, it is necessary to standardize variables. This involves renaming variables in a way that avoids conflicts. For example, if two different formulas have the same variable, they should be renamed to distinct variables.
2. Conversion to Clausal Form: Convert the given set of formulas into clausal form. Clausal form represents formulas as a disjunction (or) of literals (positive or negative atomic formulas). This step involves eliminating implications, moving negations inwards using De Morgan’s laws, and converting quantified formulas into skolemized or prenex normal form.
3. Apply Resolution: Apply the resolution rule to resolve pairs of complementary literals (literals with opposite truth values) in different clauses. The resolution process involves the following steps:

a. Select two clauses that contain complementary literals.

b. Identify a pair of complementary literals, one positive and one negative, from these clauses.

c. Create a new clause by removing the selected literals from their respective clauses and combining the remaining literals.

d. Perform standardization of variables, if necessary, by renaming variables to avoid conflicts.

e. Repeat steps a to d until no further resolutions are possible or a contradiction (an empty clause) is derived.

• Reach a Conclusion: If a contradiction (an empty clause) is derived during the resolution process, it means that the original set of formulas is unsatisfiable, and the proof is complete. If no contradiction is reached, and no further resolutions are possible, the set of formulas is satisfiable.

Resolution in Predicate Logic is a powerful and complete inference rule, meaning that if a set of formulas is valid, resolution will eventually lead to a contradiction. However, it suffers from the “combinatorial explosion” problem, as the number of clauses and literals increases exponentially with the size of the original set of formulas. Therefore, it may not be efficient for larger or more complex problems, and other proof techniques such as Semantic Tableaux or Automated Theorem Provers are often employed instead.