Sunday is a Holiday

A logic problem by Brandon Bennett

Your problem is to use propositional logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove that the reasoning is valid.

Use the following template file to create your Prover9 encoding of the problem: sundays.p9

Marks: There are two marks for each sentence, making a total of 12 marks.

Problem Statement

A1	Sunday is a Holiday.
A2	Saturday and Sunday is the weekend.
A3	On holidays the University is closed.
A4	It is the weekend.
A5	It is not Saturday.
Goal	The University is closed.

Non-Logical Vocabulary

Propositional Constants: Sunday, Holiday, Saturday, Weekend, UniversityClosed

Notes:

Note that in some contexts we can translate names of days or time periods into propositions. Thus, sometimes 'Saturday' can be translated as a proposition, i.e. as 'It is Saturday'. If we were using first-order logic we would probably treat 'Saturday' and 'Sunday' as constants and 'weekend' and 'holiday' as predicates, but for this problem you need to consider all of them as propositions which can be true or false at a given time.