Propositional Inferences Assignment 1

COMP4418, 2017–Assignment 1

Worth: 15%.
This assignment consists of three questions. The first two questions require written answers only. The third
question requires some programming.
1. [20 Marks] (Propositional Inferences)
Prove whether or not the following inferences hold in propositional logic using the truth table method.
(a) p ∨ (q ∧ r) |= (p ∨ q) ∧ (p ∨ r)
(b) |= p → (q → p)
(c) p → q |= ¬p → ¬q
(d) p → q, ¬p → ¬q |= ¬p ↔ ¬q
(e) ¬q → ¬p, ¬r → ¬q |= p → r
Prove whether or not the following inferences hold in propositional logic using resolution.
(f) p ∧ (q ∨ r) ` (p ∧ q) ∨ (p ∧ r)
(g) p ` p → q
(h) p ↔ q ` (q ↔ r) → (p ↔ r)
(i) ¬p ∧ ¬q ` p ↔ q
(j) ¬q → ¬p, ¬r → ¬q ` p → r
2. [30 Marks] (Logic Puzzle)
Daisy and Donald Duck took their nephews aged 4, 5 and 6 on an outing. Each boy wore a tee-shirt
with a different design on it and of a different colour. You are also given the following information:
• Huey is younger than the boy in the green tee-shirt
• The five year-old wore the tee-shirt with the camel design
• Dewey’s tee-shirt was yellow
• Louie’s tee-shirt bore the giraffe design
• The panda design was not featured on the white tee-shirt
(a) Represent these facts as sentences in first-order logic using the following constant symbols:
• dewey, huey and louie; the names of the nephews
• camel, giraffe and panda; the designs on the t-shirts
• green, white and yellow; the colours of the t-shirts
and the following predicates:
• age(Boy, Age)
• design(Boy, Design)
• colour(Boy, Colour)
1
(b) Using your formalisation in part (2a), is it possible to conclude the age of each boy together with
the colour and design of the tee-shirt they’re wearing? Show semantically how you determined
your answer.
(c) If your answer to part (2b) was ‘no’, indicate what further sentences you would need to add to
your formalisation so that you could conclude the age of each boy together with the colour and
design of the tee-shirt they’re wearing.
3. [50 Marks] (Automated Theorem Proving)
In 1958 the logician Hao Wang implemented one of the first automated theorem provers. He succeeded
in writing several programs capable of automatically proving a majority of theorems from the first five
chapters of Whitehead and Russell’s Principia Mathematica (in fact, his program managed to prove
over 200 of these theorems “within about 37 minutes, and 12/13 of the time is used for read-in and
print-out”). This was an impressive achievement at the time; previous attempts had only succeeded
in proving a handful of the theorems in Principia Mathematica.
Background
Wang’s idea is based around the notion of a sequent (this idea had been introduced years earlier by
Gentzen) and the manipulation of sequents. A sequent is essentially a list of formulae on either side
of a sequent (or provability) symbol `. The sequent π ` ρ, where π and ρ are strings (i.e., lists) of
formulae, can be read as “the formulae in the string ρ follow from the formulae in the string π” (or,
equivalently, “the formulae in string π prove the formulae in string ρ”).
To prove whether a given sequent is true all you need to do is start from some basic sequents and
successively apply a series of rules that transform sequents until you end up with the sequent you
desire. This process is detailed below.
Additionally, determining whether a formula φ is a theorem, is equivalent to determining whether the
sequent ∅ ` φ is true (e.g., ` ¬φ ∨ φ).
Formulae
Connectives
We allow the following connectives in decreasing order of precedence:
¬ — negation
∧ — conjunction; ∨ — disjunction (both same precedence)
→ — implication; ↔ — biconditional (both same precedence).
Formula
• A propositional symbol (e.g., p, q, . . .) is an atomic formula (and thus a formula).
• If φ, ψ are formulae, then ¬φ, φ ∧ ψ, φ ∨ ψ, φ → ψ, φ ↔ ψ are formulae.
Sequent
If π and ρ are strings of formulae (possibly empty strings) and φ is a formula, then π, φ, ρ is a string
and π ` ρ is a sequent.
2
Rules
The logic consists of the following sequent rules. The first rule (P1) gives a characterisation of simple
theorems. The remaining rules are simply ways of transforming sequents into new sequents. The
manner in which you can construct a proof for a sequent to determine whether it holds or not is given
below.
P1 Initial Rule: If λ, ζ are strings of atomic formulae, then λ ` ζ is a theorem if some atomic formula
occurs on both side of the sequent `.
In the following ten rules λ and ζ are always strings (possibly empty) of formulae.
P2a Rule ` ¬: If φ, ζ ` λ, ρ, then ζ ` λ, ¬φ, ρ
P2b Rule ¬ `: If λ, ρ ` π, φ, then λ, ¬φ, ρ ` π
P3a Rule ` ∧: If ζ ` λ, φ, ρ and ζ ` λ, ψ, ρ, then ζ ` λ, φ ∧ ψ, ρ
P3b Rule ∧ `: If λ, φ, ψ, ρ ` π, then λ, φ ∧ ψ, ρ ` π
P4a Rule ` ∨: If ζ ` λ, φ, ψ, ρ, then ζ ` λ, φ ∨ ψ, ρ
P4b Rule ∨ `: If λ, φ, ρ ` π and λ, ψ, ρ ` π, then λ, φ ∨ ψ, ρ ` π
P5a Rule `→: If ζ, φ ` λ, ψ, ρ, then ζ ` λ, φ → ψ, ρ
P5b Rule →`: If λ, ψ, ρ ` π and λ, ρ ` π, φ, then λ, φ → ψ, ρ ` π
P6a Rule `↔: If φ, ζ ` λ, ψ, ρ and ψ, ζ ` λ, φ, ρ, then ζ ` λ, φ ↔ ψ, ρ
P6b Rule ↔`: If φ, ψ, λ, ρ ` π and λ, ρ ` π, φ, ψ, then λ, φ ↔ ψ, ρ ` π
Proofs
The basic idea in proving a sequent π ` ρ is to begin with instance(s) of Rule P1 and successively
apply the remaining rules until you end up with the sequent you are hoping to prove.
For example, suppose you wanted to prove the sequent ¬(p∨q) ` ¬p. One possible proof would proceed
as follows.
1. p ` p, q Rule 1
2. p ` p ∨ q Rule P4a
3. ` ¬p, p ∨ q Rule P2a
4. ¬(p ∨ q) ` ¬p Rule P2b
QED.
However, a simpler idea (as it will involve much less search) is to begin with the sequent(s) to be proved
and apply the rules above in the “backward” direction until you end up with the sequent you desire.
In the example then, you would begin at step 4 and apply each of the rules in the backward direction
until you end up at step 1 at which point you can conclude the original sequent is a theorem.
Question Specification
In this assignment you are to emulate Hao Wang’s feats and implement a propositional theorem prover.
You may use any programming language to complete this question. You must provide a script named
assn1q3 or a Makefile that, when the command make is executed, produces an executable file assn1q3.
3
Input
The input will consist of a single sequent on the command line. Sequents will be written as:
[List of Formulae] seq [List of Formulae] To construct formulae, atoms can be any string of characters (without space) and connectives as follows:
• ¬: neg
• ∧: and
• ∨: or
• →: imp
• ↔: iff
So, for example, the sequent p → q, ¬r → ¬q ` p → r would be written as:
[p imp q, (neg r) imp (neg q)] seq [p imp r]
Your program should be called assn1q3 and run as follows:
./assn1q3 Sequent
For example
./assn1q3 [p imp q, (neg r) imp (neg q)] seq [p imp r]
Output
The first line of the output will be either true or false indicating whether or not the sequent on the
command line holds. This output is worth 40% of the total mark for this question on given and hidden
test data. The subsequent lines of output should produce a proof like the one in the Proofs section
above.
Marking for this Question
• Code: 40%
• Given test data: 20%
• Hidden test data: 20%
• Printing proofs: 20%
References
[1] Hao Wang, Toward Mechanical Mathematics, IBM Journal for Research and Development, volume
4, 1960. (Reprinted in: Hao Wang, ”Logic, Computers, and Sets”, Sciene Press, Peking, 1962. Hao
Wang, ”A Survey of Mathematical Logic”, North Holland Publishing Company, 1964. Hao Wang,
”Logic, Computers, and Sets”, Chelsea Publishing Company, New York, 1970.)
[2] Alfred North Whitehead and Bertrand Russell, Principia Mathematica, 2nd Edition, Cambridge
University Press, Cambridge, England, 1927.
4
A List of 10 Propositional Theorems
You may find it instructional to prove these by hand first.
(a) ` ¬p ∨ p
(b) ¬(p ∨ q) ` ¬p
(c) p ` q → p
(d) p ` p ∨ q
(e) (p ∧ q) ∧ r ` p ∧ (q ∧ r)
(f) p ↔ q ` ¬(p ↔ ¬q)
(g) p ↔ q ` (q ↔ r) → (p ↔ r)
(h) ` (¬p ∧ ¬q) → (p ↔ q)
(i) p ↔ q ` (p ∧ q) ∨ (¬p ∧ ¬q)
(j) p → q, ¬r → ¬q ` p → r
Assignment Submission
You will need to submit answers to Questions 1 and 2 in a PDF file named assn1.pdf along with any source
code files for Questions 3. For Question 3 you can either submit a script named assn1q3 or a Makefile that,
when make is executed, the executable file assn1q3 is generated. Your report for Question 3 in assn1.pdf
should describe the additional files you submit for this question and how they can used to replicate/generate
your results.
give cs4418 assn1 assn1.pdf assn1-q3-files
The deadline for this submission is 14:59:59am Wednesday 30 August.
Late Submissions
In case of late submissions, 10% will be deducted from the maximum mark for each day late.
No extensions will be given for any of the assignments (except in case of illness or misadventure). Read
the study guide carefully for the rules regarding plagiarism.
5