Model Checking Sum and Product

This webpage contains the implementation of the Sum and Product riddle in the model checker DEMO, and its output.

• SNP.hs specifies the Sum-and-Product problem.
• SNP.txt shows interaction with the model
• A short (6 page) paper also titled Model Checking Sum and Product explains the program SNP.hs and its output. It has been presented at the Australian AI 05 conference.
  (H.P. van Ditmarsch, J. Ruan, L.C. Verbrugge, Model Checking Sum and Product. In: S. Zhang and R. Jarvis (editors), Proceedings of the 18th Australian Joint Conference on Artificial Intelligence (AI 2005) (LNAI 3809), pages 790-795, Springer Verlag, Berlin, 2005.)
• This repository contains more information on DEMO.
• A long paper Sum and Product in Dynamic Epistemic Logic (Sept 2006) has been accepted subject to revision for the Journal of Logic and Computation and is currently under resubmission. (It contains the short paper - more or less - as Sections 7 and 8.) The program (also named) SNP.hs in the long paper contains some extra lines of code, illustrating a less efficient variant (see the paper for details).