StFX Logic Talk 1: Solving Sum-and-Product Riddle Using Public Announcement Logic

In this talk I will present a joint work with H. van Ditmarsch and R. Verbrugge. I will first introduce the problem we want to solve: the Sum-and-Product Riddle. Then I will present how to model the Sum-and-Product riddle in a modal logic called public announcement logic. This logic contains operators for knowledge, but also operators for the informational consequences of public announcements. The logic is interpreted on multi-agent Kripke models. The riddle is then implemented and its solution verified in the epistemic model checker DEMO. The results are compared with other work in epistemic model checking and the complexity is experimentally investigated for several representations and parameter settings.

Here is the Sum-and-Product Riddle:

Adam says to S and P: I have chosen two integers x, y such that 1 < x < y and x + y ≤ 100. In a moment, I will inform S only of s = x + y, and P only of p = xy. These announcements remain private. You are required to determine the pair (x, y).

He acts as said. The following conversation now takes place:
i. P says: ‘I do not know it.’
ii. S says: ‘I knew you didn’t.’
iii. P says: ‘I now know it.’
iv. S says: ‘I now also know it.’

Determine the pair (x,y).

Reference:
H.P. van Ditmarsch, J. Ruan, L.C. Verbrugge, Sum and Product in Dynamic Epistemic Logic.