Description
COL 703 Assignment 1
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.
