Applications of Resolution

Applications of Resolution

Resolution is a powerful method in formal logic used to derive conclusions from a set of premises. This method is particularly useful in both propositional and first-order logic. In this section, we will explore various applications of resolution, including automated theorem proving, logic programming, and knowledge representation.

Automated Theorem Proving

Automated theorem proving is the process of using algorithms to prove theorems automatically. Resolution is a key technique in this area. The basic idea is to transform the premises and the negation of the conclusion into a conjunctive normal form (CNF) and then apply resolution to derive a contradiction.

To illustrate this, consider the following premises:

• P1: A ∨ B
• P2: ¬A ∨ C
• P3: ¬B ∨ ¬C

We want to prove the conclusion: ¬C. We first negate the conclusion to get C and combine it with the premises:

P1: A ∨ B
P2: ¬A ∨ C
P3: ¬B ∨ ¬C
C

Next, we convert these into CNF:

P1: A ∨ B
P2: ¬A ∨ C
P3: ¬B ∨ ¬C
C

Now we apply resolution:

1. From P1 and C, we can resolve to get B.
2. Now we can resolve B with P3 to get ¬C.
3. Since we have derived ¬C, we have reached a contradiction with our assumption of C.

Logic Programming

Logic programming is a programming paradigm based on formal logic. In logic programming, programs are expressed in terms of relations, and computation is performed through logical inference. Prolog is a well-known logic programming language that uses resolution as its underlying mechanism.

In Prolog, you can define facts and rules. For example:

parent(john, mary).
parent(mary, susan).
grandparent(X, Y) :- parent(X, Z), parent(Z, Y).

This means that John is a parent of Mary, and Mary is a parent of Susan. The rule states that X is a grandparent of Y if X is a parent of Z and Z is a parent of Y. You can use resolution to query the database. For example, if you query:

?- grandparent(john, susan).

Prolog will apply resolution to find that John is indeed a grandparent of Susan by resolving the facts and the rule.

Knowledge Representation

Knowledge representation is another application of resolution. It involves encoding information in a way that a computer system can use to solve complex tasks. In artificial intelligence, knowledge representation allows systems to reason about the world and make decisions.

One common method of knowledge representation is using semantic networks or frames. However, resolution can be applied to propositional and first-order logic to represent knowledge. For example, consider the following knowledge base:

• P1: All humans are mortal.
• P2: Socrates is a human.

We want to conclude that Socrates is mortal. We can express this knowledge in logical form:

human(X) → mortal(X)
human(socrates)

To apply resolution, we can negate the conclusion:

¬mortal(socrates)

Now we have:

human(socrates) → mortal(socrates)
¬mortal(socrates)

We can rewrite the implication in CNF:

¬human(socrates) ∨ mortal(socrates)
¬mortal(socrates)

Now we can resolve:

1. From ¬human(socrates) ∨ mortal(socrates) and ¬mortal(socrates), we derive ¬human(socrates).

Limitations of Resolution

While resolution is a powerful technique, it has limitations. One major limitation is that it can be computationally expensive. The number of clauses can grow exponentially, making it difficult to find a resolution in a reasonable time. Additionally, resolution may not work well with certain types of logic, such as those that involve uncertainty or vagueness.

Another limitation is that resolution requires the knowledge to be complete. If there are missing premises, the resolution may fail to derive the correct conclusion.

Summary

• Resolution is a key technique in automated theorem proving.
• Logic programming uses resolution to infer conclusions from facts and rules.
• Knowledge representation can be enhanced using resolution to derive conclusions.
• Resolution has limitations, including computational expense and the need for complete knowledge.

Check your understanding

1. What is the process of automated theorem proving using resolution?
2. How does Prolog use resolution in logic programming?
3. What are the limitations of resolution in knowledge representation?
4. Explain how to derive a conclusion using resolution from a set of premises.