🤹🏼Formal Logic II Unit 6 – Resolution in First–Order Logic

What's Resolution All About?

• Resolution is a powerful inference rule and proof procedure used in first-order logic for automated theorem proving
• Enables the derivation of new clauses from existing clauses in a knowledge base until a contradiction is reached or no more inferences can be made
• Plays a crucial role in artificial intelligence, particularly in areas such as expert systems, natural language processing, and planning
• Operates on clauses represented in conjunctive normal form (CNF), where each clause is a disjunction of literals
• Aims to establish the unsatisfiability of a set of clauses by deriving the empty clause, denoted as $\square$, indicating a contradiction
• Provides a systematic and efficient method for determining the logical consequences of a given set of premises
• Serves as the foundation for various automated reasoning systems and has been extensively studied and refined in the field of logic and computer science

Key Concepts in First-Order Logic

• First-order logic extends propositional logic by introducing variables, quantifiers, and predicates, allowing for more expressive and flexible reasoning
• Variables (e.g., $x$, $y$, $z$) represent arbitrary objects in the domain of discourse and can be quantified using universal ($\forall$) or existential ($\exists$) quantifiers
• Predicates are symbols that represent properties of objects or relations between objects, such as $P(x)$ or $R(x, y)$
• Functions are special predicates that map objects to other objects, such as $f(x)$ or $g(x, y)$
• Terms are either variables, constants, or function applications, and they represent objects in the domain
• Formulas are constructed using logical connectives ($\land$, $\lor$, $\rightarrow$, $\leftrightarrow$, $\neg$) and quantifiers applied to predicates and terms
  • Example: $\forall x (P(x) \rightarrow Q(x))$ states that for all objects $x$, if $P(x)$ holds, then $Q(x)$ also holds
• Clauses are disjunctions of literals, where a literal is an atomic formula (predicate applied to terms) or its negation
  • Example: $\neg P(x) \lor Q(f(x))$ is a clause with two literals

The Resolution Principle Explained

• The resolution principle is an inference rule that allows the derivation of a new clause from two existing clauses containing complementary literals
• Two literals are complementary if one is the negation of the other, modulo unification (e.g., $P(x)$ and $\neg P(a)$ are complementary)
• The resolvent of two clauses is obtained by performing a resolution step:
  1. Find a pair of complementary literals, one from each clause
  2. Unify the literals by finding a substitution that makes them identical
  3. Remove the complementary literals and combine the remaining literals into a new clause
• The resolution principle is sound, meaning that if a resolvent is derived from two clauses, it logically follows from those clauses
• The resolution principle is also refutation complete, meaning that if a set of clauses is unsatisfiable, the empty clause ($\square$) can always be derived by repeatedly applying resolution
• The resolution principle forms the basis of the resolution proof procedure, which systematically applies resolution to a set of clauses until the empty clause is derived or no more resolvents can be generated

Steps in the Resolution Process

1. Convert the given first-order logic formulas into conjunctive normal form (CNF) by applying logical equivalences and quantifier elimination rules
2. Negate the goal formula (the formula to be proved) and add it to the set of clauses obtained from the premises
3. Repeatedly apply the resolution principle to the set of clauses, generating new resolvents and adding them to the clause set
   • Select two clauses with complementary literals
   • Unify the complementary literals by finding a most general unifier (MGU)
   • Generate the resolvent by combining the remaining literals from both clauses
4. Continue the resolution process until one of the following conditions is met:
   • The empty clause ($\square$) is derived, indicating that the original set of clauses is unsatisfiable and the goal formula is a logical consequence of the premises
   • No more resolvents can be generated, suggesting that the goal formula cannot be proved from the given premises
5. If the empty clause is derived, the resolution proof is complete, and the goal formula is established as a theorem
   • The resolution proof can be represented as a tree or a directed acyclic graph (DAG), with the premises as leaves and the empty clause as the root

Unification and Substitution

• Unification is the process of finding a substitution that makes two terms or literals identical
• A substitution is a mapping from variables to terms, denoted as $\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}$, where each $x_i$ is a variable and each $t_i$ is a term
• Applying a substitution to a term or literal replaces all occurrences of the variables in the domain of the substitution with their corresponding terms
• A unifier of two terms or literals is a substitution that makes them identical after applying the substitution
• The most general unifier (MGU) is a unifier that is more general than any other unifier, meaning that any other unifier can be obtained by composing the MGU with another substitution
• Unification is a key operation in the resolution process, as it allows the identification of complementary literals and the generation of resolvents
• The unification algorithm, such as the Robinson unification algorithm, is used to find the MGU of two terms or literals efficiently
  • The algorithm recursively compares the structure of the terms and builds the substitution incrementally
  • If a variable is unified with a term containing that variable, the unification fails (occurs check)
• Substitutions are applied to clauses during the resolution process to generate new clauses that are logically entailed by the original clauses

Strategies for Effective Resolution

• Set of support strategy: Maintain a set of clauses (the set of support) that are actively used for resolution, while the remaining clauses are used as a passive set
  • The set of support is initialized with the negated goal clause and any clauses derived from it
  • Resolvents are generated by resolving a clause from the set of support with a clause from either the set of support or the passive set
  • This strategy helps focus the resolution process on clauses relevant to the goal and avoids unnecessary inferences
• Unit preference strategy: Give priority to resolving clauses with a single literal (unit clauses) whenever possible
  • Unit clauses often lead to simplifications and can help prune the search space effectively
• Subsumption: Eliminate clauses that are subsumed by other clauses in the set
  • A clause $C_1$ subsumes another clause $C_2$ if there exists a substitution that makes all literals in $C_1$ appear in $C_2$
  • Subsumed clauses are redundant and can be safely removed without affecting the completeness of the resolution process
• Tautology elimination: Remove clauses that are tautologies, i.e., clauses that contain both a literal and its negation
  • Tautologies are always true and do not contribute to the resolution process
• Ordering strategies: Impose an ordering on the literals within each clause and use this ordering to guide the selection of literals for resolution
  • Examples include the lexicographic ordering or the maximum occurrence ordering
  • Ordering strategies can help reduce the number of redundant inferences and improve the efficiency of the resolution process

Common Pitfalls and How to Avoid Them

• Explosive growth of the clause set: The number of clauses generated during resolution can grow exponentially, leading to memory and computational limitations
  • Employ effective strategies like set of support, unit preference, and subsumption to control the growth of the clause set
  • Use efficient data structures and algorithms for storing and manipulating clauses
• Redundant inferences: Generating the same resolvent multiple times or deriving clauses that are subsumed by existing clauses can waste computational resources
  • Implement subsumption checks and tautology elimination to identify and remove redundant clauses
  • Maintain a cache of derived clauses to avoid regenerating the same resolvent
• Non-termination: In some cases, the resolution process may not terminate, especially when dealing with recursive or cyclic theories
  • Employ depth limits or inference bounds to restrict the length of resolution proofs
  • Use heuristics to guide the selection of clauses and literals for resolution, favoring those that are more likely to lead to the empty clause
• Ineffective clause representation: The way clauses are represented and stored can significantly impact the performance of the resolution process
  • Use efficient data structures, such as tries or hash tables, to store and retrieve clauses quickly
  • Normalize clauses by reordering literals, removing duplicates, and applying simplification rules to reduce their size and complexity
• Lack of problem-specific optimizations: General-purpose resolution strategies may not always be optimal for specific problem domains
  • Analyze the characteristics of the problem domain and develop domain-specific strategies and heuristics to guide the resolution process
  • Incorporate knowledge about the problem structure, such as symmetries or invariants, to prune the search space and improve efficiency

Practical Applications of Resolution

• Automated theorem proving: Resolution is widely used in automated theorem provers to establish the validity of mathematical statements and verify the correctness of software and hardware systems
  • Example: Proving the correctness of a sorting algorithm by encoding its properties and requirements in first-order logic and using resolution to derive the desired conclusion
• Logic programming: Resolution forms the basis of logic programming languages, such as Prolog, where programs are expressed as a set of logical clauses and queries are answered through resolution
  • Example: Implementing a expert system for medical diagnosis using Prolog, where medical knowledge is encoded as logical clauses and patient symptoms are used as queries to derive possible diagnoses
• Artificial intelligence: Resolution is employed in various AI tasks, such as planning, natural language processing, and knowledge representation and reasoning
  • Example: Using resolution to generate plans for robotic navigation by encoding the initial state, goal state, and action preconditions and effects as logical clauses
• Constraint satisfaction: Resolution techniques can be adapted to solve constraint satisfaction problems (CSPs) by encoding constraints as logical clauses and using resolution to find satisfying assignments
  • Example: Solving a scheduling problem by representing time slots, resources, and constraints as logical clauses and using resolution to find a feasible schedule
• Formal verification: Resolution is used in formal verification methods, such as bounded model checking and k-induction, to verify the properties of systems expressed in first-order logic
  • Example: Verifying the safety properties of a railway signaling system by encoding the system model and properties as logical clauses and using resolution to check for violations
• Ontology reasoning: Resolution can be applied to reason about ontologies expressed in description logics, a subset of first-order logic, to infer new knowledge and check the consistency of the ontology
  • Example: Using resolution to classify individuals in an ontology hierarchy based on their properties and relationships defined in the ontology axioms