Use Propositional Resolution to show that the clauses {p, q}, {¬p, r}, {¬p, ¬r}, {p, ¬q} are not simultaneously satisfiable.
Proof takes 8 steps including the premises and the goal.
To show that the clauses {p, q}, {¬p, r}, {¬p, ¬r}, {p, ¬q} are not simultaneously satisfiable using propositional resolution, we will perform a step-by-step proof that leads to a contradiction.
Step 1: Write down the premises
We start by writing down the given clauses:
{p, q}, {¬p, r}, {¬p, ¬r}, {p, ¬q}
Step 2: Convert the clauses into conjunctive normal form (CNF)
CNF is a standard form where each clause is a disjunction of literals (variables or negations of variables). In our case, the given clauses are already in CNF.
Step 3: Resolve clauses
We will start resolving the clauses to derive new clauses.
a) Resolve {p, q} with {¬p, r}:
To perform the resolution, we look for complementary literals in the two clauses: ¬p in {¬p, r} and p in {p, q}. When we find such literals, we can resolve them by eliminating the literals and combining the remaining literals.
The resolution leads to the new clause {q, r}.
b) Resolve {¬p, ¬r} with {p, ¬q}:
In this case, ¬p in {¬p, ¬r} and p in {p, ¬q} are complementary literals that can be resolved. The resolution leads to the new clause {¬r, ¬q}.
Step 4: Write down the derived clauses
After resolving the clauses, we now have the following derived clauses:
{q, r}, {¬r, ¬q}
Step 5: Continue resolving clauses
Now, we will continue resolving the derived clauses to obtain further clauses.
a) Resolve {q, r} with {¬r, ¬q}:
In this case, ¬r in {¬r, ¬q} and r in {q, r} are complementary literals that can be resolved. The resolution leads to an empty clause.
Step 6: Write down the derived clauses
After resolving the clauses, we now have the following derived clauses:
{}
Step 7: Determine if the empty clause is satisfiable
The empty clause is a contradiction since it expresses a statement that is always false. Thus, the empty clause is not satisfiable.
Step 8: Conclusion
Since the final result is an empty clause, it means that the original clauses {p, q}, {¬p, r}, {¬p, ¬r}, {p, ¬q} are not simultaneously satisfiable. This shows that there is no assignment of truth values to the variables p, q, r that can make all of the original clauses true at the same time.