1.4 Proof by Contradiction and Resolution

14 Questions

What is the basis of logic programming that automates proof by contradiction?

Complement rule x ∨ ¬x TRUE

What is another name for the 'law of excluded middle'?

Tertium non datur

In what type of logic is it true that for every proposition either the proposition itself or its negation is true?

Classical, two-valued propositional logic

What does one assume in a proof by contradiction when trying to prove a proposition A?

Assume that A is false

What is the purpose of obtaining an empty clause in resolution?

To falsify ¬F and prove that F is a tautology

What is the resolution rule used for in automated theorem proving?

To check whether a formula is a tautology

Which of the following is not a use of resolution as a proof method?

Checking for validity of a propositional formula

Which of the following is not a correct statement about clauses?

A clause is a propositional formula in disjunctive normal form

What is the resolvent formed from C1 =( D1 ∨ L) and C2 = (D2 ∨ ¬L)?

C = D1 ∨ D2

What is the result of applying resolution to M1 ∨ M2 ∨ M3 and ¬M2 ∨ M4?

M1 ∨ M3 ∨ M4

Which of the following is not a possible use of resolution in automated theorem proving?

To prove that a formula is satisfiable

What is the result of applying resolution to a set of clauses if it leads to an empty clause or contradiction?

The set of clauses is inconsistent

What is the purpose of the resolvent formed from two clauses?

To derive a new clause that can be used in further resolutions

What is the result of applying the resolution rule to a set of clauses?

A new set of clauses is formed

Study Notes

Resolution and Proof by Contradiction

Resolution is a method used in automated theorem proving, playing a key role in mathematics and computer science.
It is used in programming languages like Prolog, for expert systems, and for formal proof of software and hardware correctness in high-security applications.

Clauses and Resolution

A clause is a propositional formula that is a disjunction of literals.
A set of clauses can be seen as a formula in conjunctive normal form, or as the conjunction of individual clauses.
Every propositional formula can be represented as a set of clauses.

Resolution Rule

If C1 = D1 ∨ L and C2 = D2 ∨ ¬L are two clauses, then a new clause C = D1 ∨ D2 can be formed, known as the resolvent.
If resolution can be applied to derive a literal L and its negation ¬L, then the set of clauses is inconsistent.

Algorithm: Resolution Rule in Propositional Logic

Read the formula F
Negate F and bring ¬F in CNF represented as a set of clauses
While there is no empty clause and new clauses can still be formed, build the resolvent of two clauses and add it to the set of clauses
If an empty clause was created, then ¬F is falsified, and F is a tautology
Otherwise, F is not a tautology

Proof by Contradiction

Proof by contradiction is a widely used method in mathematics that can be automated with resolution.
It is based on the principle of tertium non datur, or the "law of excluded middle," which states that for every proposition, either the proposition itself or its negation is true.
To prove a proposition A using proof by contradiction, assume that A is false and deduce a contradiction to this assumption.

Example of Proof by Contradiction

Assume there is only a finite number of prime numbers, p1, …, pn.
Construct a new number p = p1 · p2 · … · pn + 1, which is not divisible by any of the finite number of primes.
This new number must be a prime itself, contradicting the assumption that there is only a finite number of primes.

Example of Resolution Algorithm

Start with the formula F = ¬x2 ∨ x1 ∧ x4 ∨ ¬x1 ∧ x2 ∧ x5 ∨ ¬x1 ∧ x3 ∨ x1 ∧ ¬x4 ∨ ¬x3 ∧ ¬x5
Apply the algorithm, combining clauses to form new resolvents
Obtain an empty clause, indicating that ¬F is falsified and F is a tautology.