The University of Melbourne
School of Computing and Information Systems
COMP30026 Models of Computation
Assignment 1, 2021
Released: 26 August. Deadline: 16 September at 23:00
Aims and Procedure
One aim of this assignment is to improve and test your understanding of propositional logic and
first-order predicate logic, including their use in mechanised reasoning. A second aim is to develop
your skills in analysis and formal reasoning about complex concepts, and to practise writing down
formal arguments with clarity.
This document is the assignment spec. There are six challenges. The first four are to be
completed on Grok, where you will find a module called “Assignment 1”. That module also
contains more detailed information about submission formats and how to submit your answers in
Grok. Your answers to Challenges 5 and 6 are to be submitted through Gradescope, for which
there is a menu item on Canvas. You are required to solve the challenges individually. You will
probably find them to be of varying difficulty, but each is worth 2 marks, for a total of 12.
Challenge 1
As a blade runner, Rick Deckard’s task is to identify replicants. These look exactly like humans,
but they have in fact been manufactured in the labs of Tyrell Corporation. Some replicants are
programmed to always speak the truth, while others are programmed to always lie. Unfortunately
the same goes for the humans that Deckard deals with: some are always truthful, and the rest
always lie. One day, Deckard interviewed two individuals, X and Y , who made these statements:
X: “Y is a truthful human”
Y : “X is a lying replicant”
Task 1A. Capture, as a single propositional formula, the information that was thereby available
to Deckard. You will need to take into account who makes each statement. Use propositional
letters as follows:
P : X is truthful R: X is human
Q: Y is truthful S: Y is human
Task 1B. Deckard, a competent logician, realised that the two statements would not allow him
to determine whether either was human or not. Determine which truth assignments to P , Q, R, S
make your formula from Task 1A true.
Task 1C. Now, Deckard later found out, from a reliable source, whether Y was truthful or not,
and based on that information, he knew exactly whether X was human and also whether Y was
human. Given this information, determine, for each of X and Y , whether they are a human or a
replicant.
Submission and marking. Your answer should be submitted on Grok. You will find the sub-
mission format explained there. You will receive some feedback from some elementary tests. These
merely check that your input has the correct format; they should not be relied upon for correctness.
We will test your solution comprehensively after the deadline. Task 1A is worth one mark, the rest
0.5 mark each.
Challenge 2
Conjunctive normal form (CNF) is an adequate representation of Boolean functions, because every
Boolean function can be written as a conjunction of disjunctions or literals. The set {∧,∨,?}
suffices to write all possible Boolean functions, that is, that set of connectives is functionally
complete. In fact, from De Morgan’s laws we can conclude that {∧,?} is a functionally complete
set of connectives, since P ∨ Q ≡ ?(?P ∧ ?Q), so that disjunction can always be translated into
negation and conjunction. Similarly {∨,?} is functionally complete.
Task 2. Show that {?, f} is functionally complete. That is, show that every propositional
formula has a logically equivalent formula that uses only variables, the “if–then” connective, and
the constant f (denoting “false”). We ask you to do this by writing a Haskell function that turns an
arbitrary propositional formula into an equivalent one that uses only? and f (plus any parentheses
or propositional letters you need).
Submission and marking. Your answer should be submitted on Grok. You will find the sub-
mission format explained there. You will receive some feedback from elementary wellformedness
checks; correctness is your responsibility. We will test your solution comprehensively after the
deadline. The mark for this challenge will be based on the proportion of test cases passed, for up
to 2 marks.
Challenge 3
j
m
i
l
o
k
n
A 7-segment display is an arrangement of seven LEDs (labelled
i–o), as shown here. Arrays of such displays are commonly used
to display characters in remote controls, blood pressure monitors,
dishwashers, and other devices. Each LED can be on or off, but
in most applications, only a small number of on/off combinations
are of interest (such as the 10 combinations that allow the display
in a digit in the range 0–9). In that case, the display can be con-
trolled through a small number of input wires. For example, four
input wires provide 24 input combinations, enough to cover the ten
different digits.
Here we are interested in using a 7-segment display for some uppercase letters. We want it to
be able to show eight different letters, namely A, B, C, D, E, F , G, and H. For example, to show
A, all the display segments, except o, should be lit up, giving the pattern . In detail, we want
the eight different letters displayed as , , , , , , , and , respectively. Since there are eight
letters, we need three input wires, modelled as propositional variables P , Q, and R. We will need
to decide on a suitable encoding of the eight letters. One possibility is to let A correspond to input
000 (that is, P = Q = R = f), B to 001 (that is, P = Q = f and R = t), and so on. If we do that,
we can summarise the behaviour of each input combination in the table below:
letter P Q R i j k l m n o display
A 0 0 0 1 1 1 1 1 1 0
B 0 0 1 1 1 1 1 1 1 1
C 0 1 0 1 1 0 0 1 0 1
D 0 1 1 1 1 1 0 1 1 1
E 1 0 0 1 1 0 1 1 0 1
F 1 0 1 1 1 0 1 1 0 0
G 1 1 0 1 1 0 0 1 1 1
H 1 1 1 0 1 1 1 1 1 0
Each of the seven segments i–o can be considered a propositional function of the variables P , Q,
and R. This kind of display can be physically implemented with logic circuitry, using circuits to
implement a boolean function for each of the outputs. Here we assume that only three types of logic
gates are available: An and-gate takes two inputs and produces, as output, the conjunction (∧) of
the inputs. Similarly, an or-gate implements disjunction (∨). Finally, an inverter takes a single
input and negates it (?). We can specify such a circuit by writing down the Boolean equations for
each of the outputs i–o. For example, segment i is turned off (is false) exactly when the input is
111. So, i can be captured as ?P ∨ ?Q ∨ ?R.
For efficiency reasons, we often want the circuit to use as few gates as possible. For example, the
above equation for i shows that we can implement this output using five gates. But i = ?(P∧Q∧R)
is an equivalent implementation, using only three gates. Moreover, the seven functions might be
able to share some circuitry. For example, if we have already implemented a sub-circuit defined by
u = Q ∧R (introducing u as a name for the sub-circuit), then we can define i = ?(P ∧ u), and we
may be able to re-use u while implementing the other outputs (rather than duplicating the same
gates). In some cases it may even be feasible to design a circuit that is not minimal for a given
function, but provides a minimal solution when all seven functions are designed.
Task 3. Design such a circuit, using as few gates as possible. You can define any number of
sub-circuits to help you reduce the gate count (simply give each a name).
Submission and marking. Your answer should be submitted on Grok. Submit a text file
circuit.txt consisting of one line per definition. This file will be tested automatically, so it is
important that you follow the notational conventions exactly. We write ? as - and ∨ as +. We
write ∧ as ., or, simpler, we just leave it out, so that concatenation of expressions denotes their
conjunction. Here is an example set of equations (for a different problem):
# An example of a set of equations in the correct format:
i = -Q R + Q -R + P -Q -R
j = u + P (Q + R)
k = P + -(Q R)
l = u + P i
u = -P -Q
# u is an auxiliary function introduced to simplify j and l
Empty lines, and lines that start with ‘#’, are ignored. Input variables are in upper case. Negation
binds tighter than conjunction, which in turn binds tighter than disjunction. So the equation for i
says that i = (?Q∧R)∨ (Q∧?R)∨ (P ∧?Q∧?R). Note the use of a helper function u, allowing j
and l to share some circuitry. Also note that we do not allow any feedback loops in the circuit. In
the example above, l depends on i, so i is not allowed to depend, directly or indirectly, on l (and
indeed it does not).
To test your equations and count the number of gates used, you can click Terminal and enter
the command test. To stop the Terminal click Stop.
There is one mark for a correct solution. An additional 0.5 is awarded if a correct solution uses
24 gates or fewer. A further 0.5 is awarded if a correct solution uses 18 gates or fewer.
Challenge 4
The logic of equality. Is it possible to assign values to the variables a, b, c, and d, so that the
formula (a=b)∧(b=c)∧(c=d)∧?(a=d) is true? How about the formula (a=c)? (?(a=b)∨?(b=c))?
These are examples of satisfiability questions in the system of equality logic. A formula in
equality logic includes a collection of variables, such as a, b, c, and d. These variables are related to
one another by equalities, such as (a=b). Equalities are assembled into formulas using connectives,
like the ones we are familiar with from propositional and predicate logic: ∧, ∨, ?,?,?, and ⊕. An
equality logic formula is satisfiable if there is some assignment of values to its variables that makes
the formula evaluate to true, under the usual semantics of equality and the logical connectives.
Task overview. In this challenge, you will complete an implementation of a satisfiability decision
procedure for equality logic formulas. The decision procedure will work as follows:
1. You will devise a way of modelling an equality logic formula as an equisatisfiable propositional
logic formula, using the strategy below.
2. You will implement this modelling strategy as a Haskell function that translates equality logic
formulas into propositional logic formulas, supported by some scaffolding code we provide.
We break this step down into four implementation tasks, described below.
3. We provide a satisfiability algorithm1 for propositional logic, which will decide whether your
propositional formula (and thus also the original equality logic formula) is satisfiable or not.
The strategy. The key to satisfying an equality logic formula in is knowing which variables to
assign to the same values. If we know whether or not each pair of variables shares a value, we
have all we need to evaluate the formula. If this information were to be encoded in propositional
logic, what propositions might we use? To encode an equality logic formula in propositional logic
is to use these propositions to capture the logical structure of the original formula, along with the
special properties of the equality relation, in a single propositional formula. The four tasks below
will guide you to capturing this strucure.
Task 4A. Using your propositional variables, implement a Haskell function to encode the logical
constraints implied by an equality logic formula’s connectives as a formula in propositional logic.
Task 4B. Equality is a reflexive relation: A variable always equals itself, so a formula like (a=a)
is always true in equality logic. Using your propositional variables, implement a Haskell function
to encode the constraints implied by this property as a formula in propositional logic.
Task 4C. Equality is also a symmetric relation: Equality can’t be true in one ‘direction’ and not
the other. (a=b) and (b=a) are equivalent in equality logic. Using your propositional variables,
implement a Haskell function to encode the constraints implied by this property as a formula in
propositional logic. Hint: Depending on your propositional variables, this may be a short formula.
Task 4D. Finally, equality is a transitive relation: Equalities chain together. If we know (a=b)
and (b=c), then we must have (a=c) too, even if this is not specified directly in an equality logic
formula. Using your propositional variables, implement a Haskell function to encode the constraints
implied by this property as a formula in propositional logic. Hint: For each individual group of
three variables2, consider all of the ways in which the transitive property could affect the formula.
Submission and marking. Your answer should be submitted on Grok. You will find the sub-
mission format explained there. You will receive some feedback from some tests that check the
output for some simple examples. These tests should not be relied upon for correctness. We will
test your solution comprehensively after the deadline. The mark for this challenge will be based
on the proportion of test cases passed, for up to 2 marks.
1In case you are curious: The algorithm uses the Tseytin transform (Assessed Worksheet 2) to efficiently convert
your propositional formula to conjunctive normal form, and then passes it to a SAT solver.
2It’s not necessary to consider every possible group of three variables that could form a transitive arrangement.
Our scaffolding code finds a sufficient list of triples, using a graph triangulation algorithm on the network of equalities
implied by the equality logic formula. All you need to do is handle these groups of three variables.
Challenge 5
Consider the four first-order predicate formulas
F1 : ?x (?u (?v (P (u, v, x)))??y (Q(x, y))) G : F1? F2
F2 : ?x (?v (?u (P (u, v, x)))??y (Q(x, y))) H : F2? F1
Task 5A. Determine whether G is valid or not. Either provide a proof that uses resolution to
show validity, or else specify an interpretation that makes G false.
Task 5B. Determine whether H is valid or not. Either provide a proof that uses resolution to
show validity, or else specify an interpretation that makes H false.
Submission and marking. Your answers to Challenges 5 and 6 should be submitted through
Gradescope as a single PDF document, no more than 2 MB in size. Marks are primarily allocated
for correctness, but elegance and how clearly you communicate your thinking will also be taken
into account.
Challenge 6
The notation we use for first-order predicate logic includes function symbols. This allows a very
simple representation of the natural numbers. Namely, for natural numbers, we use terms built
from a constant symbol (here we choose a, but any other symbol would do) and a function symbol
of arity 1 (we will use s, for “successor”). The idea is that 0 is represented by a, 1 by s(a), 2 by
s(s(a)), and so on. In general, s(x) represents the successor of x, that is, x+1. Logicians prefer this
“successor” notation, because it uses so few symbols and supports recursive definition—a natural
number is either ‘a’ (the base case), or it is of the form ‘s(. . .)’, where . . . is a term representing a
natural number. (Of course, for practical use, we prefer the positional decimal system.)
With successor notation, we can capture the usual “less than or equal” ordering of N (the set
of natural numbers) with these two axioms, where L(x, y) stands for x ≤ y:
?y(L(a, y)) (1)
?x?y(L(x, y)? L(s(x), s(y))) (2)
(1) says that 0 is smaller than or equal to any natural number, and (2) says that if x ≤ y then
x+1 ≤ y+1. Similarly, we can capture addition by introducing a predicate symbol for the addition
relation, letting P (x, y, z) stand for x + y = z:
?y(P (a, y, y)) (3)
?x?y?z(P (x, y, z)? P (s(x), y, s(z))) (4)
Turning the conjunction of (1)–(4) into clausal form, we end up with this set of clauses:
{{L(s(v1), s(v2)),?L(v1, v2)}, {L(a, v3)}, {P (s(v4), v5, s(v6)),?P (v4, v5, v6)}, {P (a, v7, v7)}}
Task 6A. Use resolution to show that
?x?y(L(s(a), x) ∧ P (y, y, x)) (5)
is a logical consequence of the axioms (1)–(4).
Task 6B. Your resolution proof will not only establish the truth of (5). The resolution proof
provides a sequence of most general unifiers, one per resolution step, and when these are composed,
in the order they were generated, you have a substitution that solves the constraint 1 ≤ x∧y+y = x.
Give that substitution and explain what it means in terms of natural numbers.
Submission and marking. Your answers to Challenges 5 and 6 should be submitted through
Gradescope as a single PDF document, no more than 2 MB in size. Marks are primarily allocated
for correctness, but elegance and how clearly you communicate your thinking will also be taken
into account.
Further Submission Advice
The deadline is 16 September at 23:00. Late submission will be possible, but a late submission
penalty will apply: a flagfall of 1 mark, and then 1 mark per 12 hours late.
Note that on Grok, “saving” your file does not mean submitting it for marking. To submit,
you need to click Mark and then Submit . You can submit as many times as you like. What gets
marked is the last submission you have made before the deadline.
For Challenges 5 and 6, if you produce an MS Word document, it must be exported and sub-
mitted as PDF, and satisfy the space limit of 2 MB. We also accept neat hand-written submissions,
but these must be scanned and provided as PDF. If you scan your document, make sure you set
the resolution so that the generated document is no more than 2 MB. The Canvas module, from
which you downloaded this document, has advice to help you satisfy the 2 MB requirement while
maintaining readability.
Being neat is easier if you type-set your answers, but not all typesetting software does a good
job of presenting mathematical formulas. The best tool is LATEX, which is worth learning if you
expect that you will later have to produce large technical documents. Admittedly, diagrams are
tedious to do with LATEX, even when using sophisticated packages such as Tikz. You could, of
course, mix typeset text with hand-drawn diagrams. In case you want to use this assignment to
get some LATEX practice, we will leave the source for this document in the Canvas module where
you find the PDF version.
Make sure that you have enough time towards the end of the assignment to present your solutions
carefully. A nice presentation is sometimes more time consuming than solving the problems. Start
early; note that time you put in early usually turns out more productive than a last-minute effort.
For Challenge 3 in particular, you don’t want to submit some “improved” solution a few minutes
before the deadline, as it may turn out to be wrong and you won’t have time to change your mind.
By submitting work for assessment you implicitly declare that you understand the University’s
policy on academic integrity and that the work submitted is your original work. You declare that
you have not been unduly assisted by any other person (collusion). In this assignment, individual
work is called for, but if you get stuck, you can use the Ed Discussion board to ask any questions
you have. As long as nobody directly gives away solutions, our discussion forum is both useful and
appropriate for this; we can all use it to support each other’s learning. If your question is simply to
clarify some aspect of the assignment, your post can be ‘public’, but if it reveals anything about your
attempted solution, make sure it is submitted as a ‘private’ post to the teaching team. Soliciting
help from sources other than the above will be considered cheating and will lead to disciplinary
action.