5.8. Key Properties of Resolution

So to begin with, let us try to understand what exactly is the resolution rule. It is a very important inference rule and it is used extensively in this programming language called PROLOG. So recall I said that PROLOG is an important programming language, which is used in AI applications. The resolution rule states that if you have two clauses C1 and C2, and a literal L present in positive form in C1 and negative form in C2, then we can conclude C' ˅ C'' where C' is the remaining part of C1 without L and C'' is the remaining part of C2 without ¬L.

This chunk introduces the resolution rule, which is a fundamental concept in logic. It describes how, if you have two clauses that contain a common literal in opposite forms (one in a positive form and one in a negative form), you can 'cancel out' that literal. The remaining parts of the clauses can then be combined using a logical OR (disjunction) to form a new clause. This approach simplifies the problem, making it easier to analyze logical propositions.

Imagine a situation where you have two teams of players in a game. Team A has a player who is a defender, and Team B has an opposing player whose role is to avoid the defender. If the defender successfully blocks the play, you can now focus on the remaining players in each team without considering that defender anymore, effectively simplifying the game situation.

In argument form the resolution rule can be stated as follows. So this is the argument form of resolution inference rule. It says that if you are given the clauses C1 and C2 where, C1 is C' ˅ L and C2 is C'' ˅ ¬L. Then based on these two premises, you can conclude the conclusion C' ˅ C''. I stress that to apply the resolution rule you need C1 and C2 to be clauses. The resolvent of the clauses C1 and C2 is C' ˅ C''.

This chunk elaborates on how to formally apply the resolution rule in logical arguments. It defines the conditions under which two clauses can be resolved and what the resulting clause (resolvent) will look like. It emphasizes that the original clauses must be in proper clause form, meaning they should adhere to specific logical structures, to be valid for this rule. Understanding how to formally apply this rule is vital for students studying logical inference and proofs.

Consider a scenario where you are resolving a dispute between two friends, each having a different perspective on an issue. By setting aside one specific disagreement (the common point of the debate), you can merge their remaining viewpoints to formulate a new consensus that both can agree upon. This is analogous to how the resolution rule combines remaining clauses after canceling out the common issues.

Since we are saying that resolution is a valid argument form, we will prove that, assume for the moment resolution is a valid inference rule. This means that we can say that the conjunction of clauses C1 and C2, where C1 and C2 have the common literal L available in positive and negative forms respectively, implies the disjunction C' ˅ C'' is a tautology.

In this chunk, the notion of 'tautology' is introduced. It states that the conclusion drawn from the resolution must always hold true. To demonstrate the validity of the resolution rule, the proof involves assessing the truth of the original clauses and showing that if both are true, then the resulting clause formed by the resolution is also true. This logical reasoning solidifies why the resolution rule is considered valid.

Think of a law that states 'If you get an A in all your classes (C1) and you do the necessary homework (C2), then you will pass the course (C').' This structure clearly shows that if the two conditions are met (A in all classes and doing homework), you are guaranteed to achieve a passing grade, thus representing a tautological outcome.

Now, next we want to see how exactly we resolve a set of clauses where we may have more than two clauses. Imagine you are given a set of n clauses and I would be interested to resolve the clauses in this set, which is often called as a resolvent of the set of clauses. The idea remains the same; we will keep on finding two clauses from this collection and keep on resolving them until we cannot proceed further.

This chunk discusses how to approach situations involving more than two clauses. The process involves building a resolution tree by continuously resolving pairs of clauses until no further resolutions are possible. It emphasizes that there's flexibility in which clauses to resolve, making the approach adaptable and dynamic in exploring various logical pathways.

Consider organizing a group project with multiple team members (n clauses). You start by tackling small issues between pairs of members, resolving their differences until all conflicts have been addressed. The goal is to reach a consensus or conclusion that brings the entire project team together, similar to how the resolution tree simplifies multiple logical statements.

The first property here is the following, imagine you are given a set of n clauses. Now, the claim here is that the empty clause or the constant False...that means it is always false. The statement here is that if the set of clauses in S is unsatisfiable, then when you build the resolution tree for resolving the set of clauses in S, you will see that the constant F appears in the tree.

This chunk explains the important property of resolution related to unsatisfiability. It indicates that if a set of clauses cannot be satisfied (impossible to assign true/false values satisfying all of them), resolving them will eventually lead to an empty clause. This outcome reinforces the understanding of when a set of arguments fails, which is crucial in logical proofs.

Think of trying to organize a fair event where every participant must agree on the same date. If there’s no common date that works for everyone, the effort to resolve the event planning leads to a state of 'nothing works'; this 'nothing' is analogous to the empty clause derived from unsatisfiable clauses.

--