Formalization of two Puzzles Involving Knowledge was written
between 1971 and 1987. It involves formalization of facts about
knowledge including both knowing what and knowing that,
how to assume and prove non-knowledge, joint knowledge and the effect of
learning a fact on the set of facts then known. A major proof was
done by Xiwen Ma, then visiting Stanford from Peking University.