## Description

1. For the sequents below, show which ones are valid and which ones aren’t:

(a) ¬p → ¬q ` q → p

(b) [0.5 marks] ¬p, p ∨ q ` q

(c) p ∨ q, ¬q ∨ r ` p ∨ r

(d) [0.5 marks] p ∧ ¬p ` ¬(r → q) ∧ (r → q)

2. Show that a formula φ is valid iff > ≡ φ, where > is an abbreviation for an instance p ∨ ¬p of LEM.

3. [1 marks] Let us introduce a new connective φ ↔ ψ which should abbreviate (φ → ψ) ∧ (ψ → φ).

Design introduction and elimination rules for ↔ and show that they are derived rules if φ ↔ ψ is

interpreted as (φ → ψ) ∧ (ψ → φ).

4. Prove the validity of the following sequents:

(a) ` ¬p → (p → (p → q))

(b) p ∧ q ` ¬(¬p ∨ ¬q)

(c) [0.5 marks] (p → r) ∧ (q → r) ` p ∧ q → r

(d) [0.5 marks] p → q ∧ r ` (p → q) ∧ (p → r)

5. Write a python program that takes two inputs: i) a formula file, containing a CNF formula in DIMACS

format, and ii) a proof file that contains a resolution proof, and prints “correct” if the resolution proof

is correct, and “incorrect” otherwise. The proof file contains a line for each application of the resolution

rule, in the following format:

ip jf li1 li2 … lik 0

which means that the clause in line i of the proof file (denoted by the letter ‘p’ after the number i) and

j of the formula file (denoted by the letter ‘f’ after the number j) have been resolved to get a clause

with the literals li1

, li2

, . . . , lik

(for example, 3p 7f 2 -4 5 0 denotes that the clause in line 3 of the

proof file and line 7 of the formula file have been resolved, and the resulting clause is (p2 ∨ ¬p4 ∨ p5)

assuming pi

is the name of the i

th variable).

You are required to submit the following:

(a) [1.5 marks] Your code, along with a README file containing instructions run the code.

(b) [0.5 marks] A formula file that has at least 5 different clauses, and three proof files – two

correct, and one incorrect – such that each proof file has at least four lines, and no two lines in

any single file resolve the same two clauses.

Here’s a sample formula:

c CNF formula (p1 ∨ !p2) ∧ (p2 ∨ p3) ∧ (!p1 ∨ !p2 ∨ p3) ∧ (!p3)

p cnf 3 4

1 -2 0

2 3 0

-1 -2 3 0

-3 0

And, here is a sample proof :

3f 4f 1 3 0

4f 5f -1 3 0

1p 2p 3 0

6f 3p 0

Note that this proof is correct (we have seen this example in the class), and your code should print

“correct” for the above inputs.

6. Find a propositional logic formula φ which contains only the atoms p, q, and r, and which is true only

when p and q are false, or when ¬q ∧ (p ∨ r) is true.

7. [1 marks] An adequate set of connectives for propositional logic is a set such that for every formula

of propositional logic there is an equivalent formula with only connectives from that set. For example,

{¬, ∨} is adequate. Is {↔, ¬} adequate. Justify your answer. Recall that φ ↔ ψ is interpreted as

(φ → ψ) ∧ (ψ → φ).

8. Show that the following sequents are not valid by finding a valuation in which the truth values of the

formulas to the left of ` are T and the truth value of the formula to the right of ` is F.

(a) ¬p ∨ (q → p) ` ¬p ∧ q

(b) [0.5 marks] ¬r → (p ∨ q), r ∧ ¬q ` r → q

(c) p → (¬q ∨ r), ¬r ` ¬q → ¬p

(d) [0.5 marks] p → (q → r) ` p → (r → q)

9. Give a natural deduction proof of PBC using only basic rules.