An Appointment

A logic problem by Adam Richard-Bollans

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: appointment.p9

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

Problem Statement

A1	If Alba is not late to her appointment, the optician will be happy.
A2	Alba is early to her appointment.
A3	If Alba is early then Alba is not late.
Goal	The optician is happy.

Non-Logical Vocabulary

Propositional Constants: AlbaLate, OpticianHappy, AlbaEarly

Notes:

A3 encodes part of the relationship between the meaning of `early' and `late'. If we simply remove this statement, Prover9 won't find a proof as it doesn't know what `early' or `late' mean.