Artificial Intelligence - Resolution in First Order Logic (FOL)

---

---

What is Resolution

Resolution is a logical method that is used to validate statements by showing that assuming the negation leads to a contradiction. Essentially, it assesses the truth of a claim by presuming it is false and then proving that this assumption is impossible.

What is Resolution in First-Order Logic

A resolution is a rule in first-order logic (FOL) that allows us to derive new conclusions from previously established data. According to the concept of proof by contradiction, if assuming something is incorrect results in a contradiction, the assumption must be true.

The resolution approach is widely employed in logic-based problem solving and automated reasoning because it produces systematic, thorough, and efficient proofs of logical statements.

Why Do We Use Resolution

Resolution is commonly used in various fields of artificial intelligence and automated reasoning. Here are some key reasons for choosing resolution −

• Prove Statements Logically Resolution uses contradiction to assess if a statement is true or false.

• Automate Logical Reasoning - Allows computers to automatically draw conclusions from provided facts.

• Solve Problems in AI and Logic Programming - Used in Prolog and other AI applications for rule-based reasoning.

• Ensure Consistency in Knowledge-Based Systems - Assists in detecting inconsistencies and maintaining valid information.

• Verify Software and Systems - Ensures that software, security protocols, and hardware are working properly.

Key Components in Resolution

Resolution in First-Order Logic (FOL) depends on several key components that enhance the effectiveness of the inference process. They are −

Clause

A clause is a dis-junction that serves as a fundamental unit in resolution-based proofs. Following are the examples to better understand the Clauses −

• P(x)¬Q(x) → This expression consists of two literals linked by OR ().

• ¬ABC → This expression includes three literals, meaning at least one of them must be true.

Literals

A literal is either the atomic proposition (fact) or its negation. Literals are the building blocks of clauses. Here is an example of literals.

• P(x) is a positive literal that is either true or false.

• ¬Q(y) is a negative literal which is the negation of a fact.

Unification

Unification is the operation of two logical expressions by determining the correct substitutions for the variables to make both expressions equal. Here is an example of Unification.

• Let us consider two predicates − Predicate 1: Loves (x, Mary).

• Predicate 2: Loves (John,y).

To unify these two predicates, we have to find the substitutes for x and y such that they become identical. Substituting x=John and y=Mary gives us Loves(John, Mary). So, after unification, both predicates are the same.

Substitution

Substitution is the replacement of variables by definite values or words in a logical formulation for more specific expression. It is used in unification, resolution, and inference rules to make logical assertions more specific. Below is the example of substitution −

• Consider this predicate with a function: Teaches(Prof, Subject). Substituting = {Prof/Dr. Smith, Subject/Mathematics} yields the results in Teaches(Dr. Smith, Mathematics).

Skolemization

Skolemization is the process of removing existential quantifiers () by introducing Skolem functions or constants.

• Let us consider a statement, x y Loves(x, y), which means "for every x, there exists some y such that x loves y."

• To remove y, we introduce a Skolem function f(x), resulting in x Loves(x, f(x)), where f(x) represents a specific person that x loves, making the statement fully quantifier-free.

Steps for Resolution in First-Order Logic (FOL)

The resolution process involves systematically modifying logical statements and utilizing unification and resolution principles to either derive a contradiction or establish the desired outcome. Below are the key steps involved in FOL resolution −

• Convert statements to First-Order Logic (FOL) and express the given information using FOL notation.

• Convert FOL sentences into Clausal Form (CNF) by removing implications, moving negations inward, standardizing variables, applying Skolemization, and converting to conjunctive normal form.

• Negate the assertion to be verified - Assume the negation of the goal and include it in the list of clauses.

• Apply Unification: Find relevant variable substitutions to make literals identical.

• Use the Resolution Rule: Identify complementing literals and resolve them to create new clauses.

• Repeat until a contradiction or proof is found. Resolve until an empty clause () is derived (contradiction) or the goal statement is proven.

Example for Resolution in First-Order Logic

Let us consider the following statements −

• Every employee of Tutorials Point is knowledgeable.

• John is an employee of Tutorials Point.

• Prove that John is knowledgeable.

Step1: Convert statements to First-Order Logic (FOL)

• Statement 1: x (Employee(x, TutorialsPoint) → Knowledgeable(x))

• Statement 2: Employee(John, TutorialsPoint)

• Statement to Prove: Knowledgeable(John)

Step2: Convert FOL sentences into Clausal Form (CNF)

Remove Implications:

• ¬Employee(x, TutorialsPoint) Knowledgeable(x)

• Employee(John, TutorialsPoint)

Step3: Negate the Assertion to be Verified

To apply proof by contradiction, we assume the negation of the goal statement and add it to the set of clauses.

• Negated Goal: ¬Knowledgeable(John)

Step4: Apply Unification

Unification is performed to match variables and make expressions identical, allowing further resolution.

• Unify: x = John in Clause 1

• Substituting in Clause 1: ¬ Employee(John, TutorialsPoint) Knowledgeable(John)

Step5: Use the Resolution Rule

Resolution is applied to eliminate complementary literals and derive a new clause.

• Resolving Clause 2 (Employee(John, TutorialsPoint)) with Clause 1 (¬Employee(John, TutorialsPoint) Knowledgeable(John))

• Employee(John, TutorialsPoint) and ¬Employee(John, TutorialsPoint) cancel out.

• New Clause: Knowledgeable(John)

• The new clause Knowledgeable(John) is derived, bringing us closer to proving the goal.

Step6: Repeat Until a Contradiction or Proof is Found

The final resolution step confirms the goal by contradiction. Resolving Clause 3 (¬Knowledgeable(John)) with Knowledgeable(John). The literals cancel out, resulting in an empty clause ({}).

• Since an empty clause is derived, it confirms that the original goal (Knowledgeable(John)) is true.

Examples of Resolution in AI

Resolution plays a crucial role in various AI applications as it enables automated reasoning and logical inferences. Here are some key examples of how resolution is applied in AI.

• AI has an impact on Automated Theorem Proving - Resolution to prove mathematical theorems without human intervention. Programs like the Lean Theorem Prover and the Coq Proof Assistant use Resolution to check mathematical proofs.

• Expert Systems - AI systems use rule-based reasoning to draw logical conclusions. In medical diagnosis, expert systems like MYCIN use resolution to guess diseases based on symptoms and patient information.

• Natural Language Processing (NLP) - Resolution helps to break down and show meaning. AI-based NLP models such as IBM Watson and Google's BERT, apply resolution methods to find logical connections between words and boost language understanding.

Limitations of Resolution

Below are some key limitations of the resolution method in logical inference

• Computational Complexity: It produces numerous intermediate clauses, making it slow when dealing with large knowledge bases.

• Lack of Expressiveness: Transforming to CNF limits the expressiveness of some logical propositions.

• Handling Infinite Domains: There are challenges with recursive definitions and infinite problem sets.

Resolution is inherently monotonic, which means that once facts are introduced, they cannot be removed. This characteristic makes it unsuitable for managing dynamic or uncertain knowledge where conclusions might need to be adjusted.