Reasoning about knowledge with hybrid modal logic

Puzzle

Student picks two numbers between 2 and 100, and gives their sum to professor Sum and their product to professor Product.

Professor Product takes a look at the product and says:
I don't know what the numbers are.

Professor Sum replies:
I knew you wouldn't know.

Professor Product replies:
But now I do.

Professor Sum replies:
Now I do too.

Can you figure out the numbers?

Solution

The solution, written in the executable specification language AsmL, is based on a simple global model checker for a subset of multimodal hybrid logic with the downbinder operator.

Requirements for compiling and running the executable specification are:

• AsmL compiler
• Microsoft Word 2002 or newer

Once you have the AsmL compiler installed, you can compile and execute the specifications directly from Microsoft Word:
[ Puzzle.doc ]

You can also browse the specifications with any web browser:
[ HTML, Puzzle.pdf ]