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.
.dvi, .pdf and .ps versions are also available.
The number of hits on this page since 1996 May 14.