I'm working on LPL's Exercise 11.21, which asks to provide translations of the English language sentences into First Order Logic sentences. Unlike the majority of exercises in the book, as I understood, this one requires an experienced instructor to check them as it cannot be verified by the automatic grading system which governs the rest of the course.
For that reason I'd like to ask you to check my translations here for the 2 sentences, for which I received "We could not determine whether your sentence was correct" from the grading system.
The predicates to be used
- Pet(x) – x is a pet
- t < t' – t is earlier than t'
- Hungry(x, t) – x was hungry at time t
- Owned(x, y, t) – x owned y at time t
- Gave(x, y, z, t) – x gave y to z at time t
Exercise 11.21
Translate the following into FOL.
7) If Max ever gave Claire a pet, she owned it then and he didn't.
9) Max fed all of his pets before Claire fed any of her pets.(Assume that "Max's pets" are the pets he owned at 2:00, and the same for Claire.)
My (proposed) solutions
7) $$
\forall x \forall t \Bigg( Pet(x) \rightarrow \\
\bigg(
\exists u
\big( Gave(max, x, claire, u) \land u < t
\big)
\rightarrow \\
\Big( Owned(claire, x, t) \land \neg Owned(max, x, t)
\Big)
\bigg)
\Bigg)
$$
9)
$$ \exists t \Bigg( \\
\forall x
\Big(
\big(
Owned(max, x, 2:00) \land Pet(x)
\big)
\rightarrow
\exists u
\big(
u < t \land Fed(max, x, u)
\big)
\Big)
\\ \land \\
\neg \exists x
\Big(
Owned(claire, x, 2:00) \land Pet(x) \land
\exists u \big(
u < t \land Fed(claire, x, u)
\big)
\Big)
\Bigg) $$
Best Answer
For 7): your translation would mean that once Max gave a pet to Claire, Claire will own it forever, and Max will never own it again. But Claire could of course give the pet back to Max at some later point.
So, I think what they mean is that at the very time Max gives a pet to Claire, Claire owns it, and Max does not. This is why I think they used '... owned it then ...', i.e. owned it at that very time point ... because for all time points after that you can't say anything.
So, I would try:
$$\forall x \forall t ((Pet(x) \land Gave(max, claire, x, t)) \rightarrow (Owned(claire,x,t) \land \neg Owned(max,x,t)))$$
Your 9) looks fine to me .... If I were the instructor, I would certainly count it as correct. And remember this: the automated grading system sometimes will indeed have to pass off a proposed translation to the instructor, because the grading system has to test for logical equivalence between the proposed translation and whatever translation the programmers gave it. And testing for logical equivalence is an undecidable problem (it's as hard as the Halting problem, it turns out). So, they must have given the algorithm a timer, and when it times out, you get the message that you did.