Aims & 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 which you will find in the remainder of this document.  Your answers to Challenge 5 and Challenge 6 are to be submitted through Gradescope, for which there is a menu item on Canvas.  The remaining challenges 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.

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 – Predictably Inconsistent Weather

The city of Melbourne, Australia is infamous for its predictably inconsistent weather. The mobile apps Parrot and Carrot compete to predict the correct weather over the next three days.  Mel- bourne’s weather has a habit of making a fool of the apps’ developers, such that at any time, only one of the two apps makes a correct prediction.

Despite this, Harald still can use this information to get accurate weather forecasts for the week, so that they don’t get wet on their commutes to-and-from university. On a Monday, Harald checks both the Carrot and Parrot apps, where they make the following predictions:

Carrot: “It will rain on Tuesday and Wednesday.”

Parrot:    “If it rains on Monday, it will rain on Wednesday.”

Task 1A. Capture, as a single propositional formula, the information that was thereby available

to Harald. You will need to take into account which app makes each prediction. Use propositional

letters as follows:

C ∶    Carrot’s prediction is correct       P ∶    Parrot’s prediction is correct

M ∶    It rains on Monday       T ∶    It rains on Tuesday ∶    It rains on Wednesday

Task 1B. Harald tries to determine the weather forecast for the week from those two predictions, but realises they do not yet have enough information.   Determine which truth assignments to C, P , M, T , make your formula from Task 1A true.

Task 1C. Harald opens their window blinds and looks outside to check for any chance of rain. Based on that information, they now knew exactly what the weather would be for Monday, Tuesday and Wednesday. Given this information, determine, for each of Monday, Tuesday and Wednesday, whether it rains or not.

Submission and Marking: Your answer should be submitted on  Grok.   You will find the submission 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 1

mark, the rest are worth 0.5 marks each.

Challenge 2 – Negative Implications

We have seen that implication can be re-written into an equivalent formula using the following equivalence

F ⇒ G ≡  ¬(F ∧ ¬G)                                                            (2.1)

In this challenge we will generalise this result to rewrite all of the connectives we have seen using ∧ and ¬ . To this effect, we will show that {∧, ¬} is functionally complete as we can represent all formulas using only ∧ and ¬ .

Task 2A. Using the equivalence defined in (2.1), re-write the following formula to remove all instances of the ⇒ connective. You must not perform any other transformations.

(¬P ⇒ (¬Q ∧ Q ⇒ f))  ⇒ (((P ⇒ ¬( ⇒ Q)) ∧ ¬P)  ⇒ ¬(P ⇒ ¬( ⇒ Q)))           (2.2)

Task 2B. The formula  (2.2) can be simplified.   Using only the equivalences  (2.1) and  (2.3)– (2.5) you can simplify your answer for Task 2A. Provide the most simplified formula using (2.1) and (2.3)– (2.5), with no instances of ⇒ .  This should contain the smallest number of connectives possible.

F ∧ G ≡ G ∧ F                                                          (2.3)

¬F ∧ (F ⇒ G)  ≡  ¬F                                                               (2.4)

¬¬F ≡ F                                                                  (2.5)

Task 2C. Generalising the re-writing rule (2.1), we can re-write all other connectives using only ∧ and ¬ .  Write a Haskell function that can re-write any formula into an equivalent formula that uses only ∧ , ¬ , and any variables.  Your function should not produce any double-negatives, such

as ¬¬P .

Submission and Marking: Your answer should be submitted on  Grok.   You will find the submission 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 2A and Task 2B are worth 0.5 marks each for a correct answer; Task 2C is worth 1 mark based proportionally on the number of passed test cases.

Challenge 3 – Logic on Display