Resolution in Propositional Logic

Resolution in Propositional Logic

Resolution is a powerful rule of inference used in propositional logic. It allows you to derive new clauses from existing ones. This process is essential in automated theorem proving and artificial intelligence.

Understanding Clauses

A clause in propositional logic is a disjunction (OR operation) of literals. A literal is either an atomic proposition or its negation. For example, the clause A ∨ B contains the literals A and B. The clause ¬C is a single literal.

The Resolution Rule

The resolution rule states that if you have two clauses, one containing a literal and the other containing its negation, you can derive a new clause. The general form of the resolution rule is:

If you have:

C1: A ∨ B

C2: ¬A ∨ D

You can derive:

C3: B ∨ D

This is done by resolving on the literal A.

Example of Resolution

Let's consider the following clauses:

C1: P ∨ Q

C2: ¬P ∨ R

To resolve these clauses, identify the complementary literals. Here, P in C1 and ¬P in C2 are complementary. Applying the resolution rule, we derive:

C3: Q ∨ R

Thus, from clauses C1 and C2, we have derived a new clause C3.

Multiple Resolutions

You can apply resolution multiple times to derive new clauses. For example, consider the following clauses:

C1: A ∨ B

C2: ¬A ∨ C

C3: ¬B ∨ D

First, resolve C1 and C2:

C4: B ∨ C

Next, resolve C4 and C3:

C5: C ∨ D

From these resolutions, we derived C4 and then C5.

Completeness of Resolution

Resolution is complete for propositional logic. This means that if a set of clauses is unsatisfiable (there is no assignment of truth values that makes all clauses true), resolution will eventually derive the empty clause, denoting a contradiction.

Example of Completeness

Consider the clauses:

C1: A ∨ B

C2: ¬A

C3: ¬B

We can resolve C1 and C2 to derive:

C4: B

Next, resolve C4 with C3:

C5: ⊥ (empty clause)

The empty clause indicates that the original set of clauses is unsatisfiable.

Applications of Resolution

Resolution is used in various fields, including:

• Automated Theorem Proving: It helps in proving theorems automatically by deriving contradictions.
• Artificial Intelligence: It is used in knowledge representation and reasoning.
• Logic Programming: Languages like Prolog use resolution as a fundamental mechanism for inference.

Transforming to Conjunctive Normal Form

Before applying resolution, you must convert your clauses to conjunctive normal form (CNF). A formula is in CNF if it is a conjunction (AND operation) of one or more clauses, where each clause is a disjunction of literals.

Example of CNF Conversion

Consider the formula:

(A ∧ B) → C

To convert this to CNF, follow these steps:

1. Rewrite the implication:

¬(A ∧ B) ∨ C

2. Apply De Morgan's Law:

¬A ∨ ¬B ∨ C

This is now in CNF as it is a single clause.

Self-Check Questions

1. What is a clause in propositional logic?

2. Describe the resolution rule.

3. What does it mean for resolution to be complete?

4. How do you convert a formula to conjunctive normal form?

Summary

• Resolution is a rule of inference in propositional logic.
• A clause is a disjunction of literals.
• The resolution rule allows the derivation of new clauses.
• Resolution is complete for propositional logic.
• Converting to CNF is necessary before applying resolution.