Resolution in Artificial Intelligence

This topic reveals:

  • Meaning of Resolution

  • Syntax of Resolution

  • Resolution in FOPL

  • Example

  • Types of Resolution


Resolution is a fundamental inference rule used in automated reasoning and logic-based AI systems. It is a technique employed in propositional logic and first-order logic to derive new logical statements or facts from existing ones. Resolution plays a crucial role in logic programming, theorem proving, and knowledge representation.

The concept of resolution involves the following steps:

1. Clause Representation: Logical statements or facts are typically represented as clauses in first-order logic. A clause is a disjunction of literals, where a literal is either an atomic proposition or its negation. For example, (p ∨ q) represents the clause "p or q."

2. Unification: Before applying resolution, the clauses involved must be unified. Unification is the process of finding substitutions for variables such that two clauses can be made identical. Variables in the clauses are matched and instantiated to specific terms.

3. Resolution Rule: The resolution rule states that if two clauses contain complementary literals (one positive and one negative), they can be resolved to derive a new clause. The resolution process combines the two clauses by removing the complementary literals.

4. Generating New Clauses: The resolution process is repeated by selecting pairs of clauses and applying the resolution rule until no new clauses can be derived. This iterative process continues until all possible combinations are exhausted.

5. Contradiction Detection: If, during the resolution process, an empty clause (a clause with no literals) is derived, it indicates a contradiction in the set of initial clauses. This contradiction implies that the original set of statements is inconsistent or unsatisfiable.

Resolution is a sound inference rule, meaning that if a statement can be derived using resolution, it is logically valid. However, it is not complete, as there may be valid statements that cannot be derived using resolution alone. To achieve completeness, additional techniques such as backtracking, strategies, or heuristics are often employed.

Overall, the resolution provides a systematic and efficient method for logical inference, enabling AI systems to reason, deduce, and derive new knowledge from existing information.

Syntax of Resolution

The syntax of resolution is based on clauses and literals, which are the building blocks of logical statements. Here's an outline of the syntax involved in the resolution process:

1. Clause: A clause is a disjunction of literals and is typically represented as a set of literals connected by logical OR (∨) operators. The syntax of a clause is as follows:
   - Clause: Literal1 ∨ Literal2 ∨ ... ∨ LiteralN

2. Literal: A literal is a basic atomic proposition or its negation. It can be represented as a predicate applied to a set of arguments or its negation. The syntax of a literal is as follows:
   - Literal: Predicate(Argument1, Argument2, ..., ArgumentN)
   - Negated Literal: ¬Predicate(Argument1, Argument2, ..., ArgumentN)

3. Resolution Rule: The resolution rule combines two clauses by removing complementary literals. The syntax of the resolution rule is as follows:
   - Clause1: Literal1 ∨ Literal2 ∨ ... ∨ LiteralN
   - Clause2: LiteralX ∨ ¬LiteralY
   - Resolution: (Clause1 - {LiteralX}) ∪ (Clause2 - {¬LiteralY})

4. Empty Clause: An empty clause represents a contradiction and indicates that the set of initial clauses is inconsistent or unsatisfiable. The syntax of an empty clause is an empty set of literals: {}.

5. Unification: Unification is the process of finding substitutions for variables in literals or clauses such that they can be made identical. It involves matching variables and instantiating them with specific terms.

The syntax of resolution can vary slightly depending on the specific logic notation or inference system being used. The examples above represent a general form of syntax commonly used in resolution-based reasoning.

It's important to note that the actual implementation of resolution may involve additional components such as indexing mechanisms, strategies for selecting clauses, and conflict resolution strategies. These elements can vary based on the specific algorithm or system used for automated reasoning and theorem proving.

Resolution in First Order Predicate Logic(FOPL)

Certainly! Let's demonstrate the resolution process using predicate logic. Consider the following two clauses:

Clause 1: ¬p(x) ∨ q(a)
Clause 2: ¬q(y) ∨ r(y)

To apply resolution, we need to unify the clauses by matching variables and literals. In this case, we can instantiate x in Clause 1 with the term a and instantiate y in Clause 2 with the term a, resulting in the unified clauses:

Unified Clause 1: ¬p(a) ∨ q(a)
Unified Clause 2: ¬q(a) ∨ r(a)

Now, we can apply the resolution rule by finding complementary literals between the unified Clause 1 and unified Clause 2. In this case, the complementary literals are q(a) and ¬q(a).

Using the resolution rule, we can derive a new clause by removing the complementary literals:

New Clause: ¬p(a) ∨ r(a)

The new clause, ¬p(a) ∨ r(a), is the result of applying resolution to the original clauses. It represents a logical consequence that can be inferred from the initial statements.

Resolution in predicate logic involves unifying clauses, applying the resolution rule to find complementary literals, and generating new clauses. The process is iterative, and it continues until no further resolutions can be made or until an empty clause is derived, indicating a contradiction.

Note that in predicate logic, unification may involve matching and instantiating not only variables but also predicates and their arguments to establish consistency between clauses. The resolution process extends to more complex scenarios with multiple predicates, quantifiers, and logical connectives.

Types of Resolution

In the field of artificial intelligence (AI), there are different types of resolution techniques used for automated reasoning and logical inference. Here are two common types of resolution in AI:

1. Propositional Resolution:
   Propositional resolution, also known as binary resolution, is a type of resolution that operates on propositional logic, where statements are represented using propositional variables and logical connectives such as AND, OR, and NOT. Propositional resolution is applied to sets of propositional clauses and involves the resolution rule that combines two clauses by eliminating complementary literals.

2. First-Order Resolution:
   The first-order resolution, also known as a resolution in first-order logic, extends resolution to first-order predicate logic, which includes quantifiers (such as "for all" and "exists") and variables. First-order resolution is used for reasoning and inference in more expressive logic systems. It involves unifying and matching predicates, applying the resolution rule, and generating new clauses based on the unified and resolved literals.

Both propositional resolution and first-order resolution are integral parts of automated reasoning systems, theorem provers, and logic programming languages. These resolution techniques allow AI systems to perform logical deduction, inference, and knowledge representation.

It's worth noting that there are various specialized versions and extensions of the resolution, such as resolution with equality, linear resolution, ordered resolution, and more. These variants introduce additional features or restrictions to the resolution process to enhance efficiency, address specific inference problems, or handle particular logical constructs.


Link to Unification Concept