Question

(a) Show that if \(r\) is the resolvant of two clauses \(c_{1}, c_{2}\) on proposition letter \(p,\) then $$ \left\\{c_{1}, c_{2}\right\\} \models r $$ (Hint: For each interpretation, break into cases, depending on whether \(p\) is \(T\) or \(F\) in each interpretation.) (b) Prove that if there is a resolution refutation of a set \(S\) of clauses, then \(S\) is unsatisfiable. (Hint: Use strong induction on the length of the resolution refutation.)

Short answer

(a) Resolvents are true under interpretations satisfying both clauses. (b) Refutation proves unsatisfiability by generating a contradiction.

Step-by-step solution

Understanding Clauses and Resolvents

In a logical system, a clause is a disjunction of literals. If we have two clauses, \( c_1 = p \lor A \) and \( c_2 = eg p \lor B \), where \( A \) and \( B \) are disjunctions of other literals, their resolvent is formed by resolving the common literal (in this case, \( p \) and \( eg p \)) to produce the clause \( r = A \lor B \).

Validating the Resolvent Case for Proposition Letter \( p \)

Consider each possible truth value of \( p \).- **Case 1:** \( p = T \). If \( p \) is true, then \( c_2 \) must be satisfied by \( B \) because \( eg p \) is false. Hence, \( B = T \), and \( r \), the disjunction \( A \lor B \), is true.- **Case 2:** \( p = F \). If \( p \) is false, then \( c_1 \) must be satisfied by \( A \) because \( p \) is false. Hence, \( A = T \), which makes \( r \), the disjunction \( A \lor B \), true.

Conclusion of Part (a)

Since in both cases \( r = A \lor B \) is true, we conclude that for any interpretation where both \( c_1 \) and \( c_2 \) hold, \( r \) also holds. Thus, \( \{ c_1, c_2 \} \models r \).

Understanding Resolution Refutation

A resolution refutation of a set \( S \) of clauses is a derivation of the empty clause \( \bot \) using resolution steps. The empty clause represents a contradiction, thereby indicating unsatisfiability.

Strong Induction on Resolution Refutation Length

Use strong induction on the number of resolution steps required to derive \( \bot \) from \( S \).- **Base Case:** If \( \bot \) is derived in a single step from \( c_i \) and \( c_j \), then \( c_i \) and \( c_j \) must be a contradiction, showing that \( S \) is unsatisfiable.- **Inductive Step:** Assume any set \( S' \) of clauses that can be refuted in \( n \) steps is unsatisfiable. If \( S \) can be refuted in \( n+1 \) steps by resolving \( c' \) with another clause, then the set excluding \( c' \) is unsatisfiable by the induction hypothesis. Adding \( c' \) would make \( \bot \) in \( n+1 \) steps, showing \( S \) is unsatisfiable.

Conclusion of Part (b)

Thus, by induction, any set \( S \) of clauses for which a resolution refutation exists must be unsatisfiable, as generating the empty clause implies a logical contradiction in \( S \).

Key concepts

Clauses in Logic

In propositional logic, a clause is essentially a group of statements, known as literals, that are combined using the logic operator 'or' (denoted as \( \lor \)). A literal can be a proposition variable itself, like \( p \), or its negation, \( eg p \). Think of a clause as a way of expressing multiple possibilities within one statement, where at least one of these possibilities must be true.

Consider the example clauses: \( c_1 = p \lor A \) and \( c_2 = eg p \lor B \). Here, \( A \) and \( B \) are other disjunctions of literals. The logic of these clauses revolves around \( p \), where each clause expresses what should hold if \( p \) or \( eg p \) is true. When two clauses share a literal like this, we can create what's known as a resolvent — a new clause that retains the truth of the original pair.

The resolvent takes all the remaining parts of each clause (after resolving the shared literal) to create a new expression: \( r = A \lor B \). This resolvent maintains truth based on the original conditions of \( c_1 \) and \( c_2 \), ensuring that logical consistency is preserved.

Resolution Refutation

Resolution refutation is a powerful method used in logic for demonstrating that a set of clauses is unsatisfiable. In simple terms, unsatisfiability means there is no possible way to assign true or false values to the variables such that all the clauses in the set hold true simultaneously.

The core idea of resolution refutation is to systematically apply resolution to resolve pairs of clauses until the empty clause, often symbolized as \( \bot \), is derived. This empty clause represents a contradiction since it signifies a situation where none of the options within it can be true. As such, the presence of \( \bot \) materializes this infeasibility, thereby proving unsatisfiability.

Resolution steps involve selecting pairs of clauses that share a complementary pair of literals — such as \( p \) in one clause and \( eg p \) in another. Resolving this yields a new clause that excludes the complementary pair while retaining other literals. Continuously applying this technique until reaching the empty set signifies that the initial set of clauses cannot all be true together, leading to the confirmation of unsatisfiability.

Strong Induction

Strong induction is a mathematical proof technique particularly useful when dealing with propositions that depend on multiple prior cases to show that a statement holds true. Unlike simple induction, strong induction allows the assumption of all preceding cases as being true to prove the next step. This approach is vital in scenarios like resolution refutation where the truth or unsatisfiability of certain combinations of clauses relies on all prior derived information.

When applying strong induction to resolution refutation, our base case considers deriving the empty clause \( \bot \) directly from two clauses that inherently contradict each other, establishing immediate unsatisfiability. The inductive step follows by assuming any set of clauses that can be resolved in \( n \) steps proves unsatisfiable. We then show that resolving an additional clause to derive \( \bot \) in \( n+1 \) steps remains unassailable.

This method ensures that if a resolution refutation for any given set of clauses exists, proving \( \bot \), then the original set was unsatisfiable. By proving for all prior steps, strong induction guarantees each progression maintains the foundational notion of unsatisfiability, reinforcing logical deduction.