Deep semantic embedding of PSL (Sugar 2.0) in HOL

The main properties proved so far are here.

The full details are in the HOL script files below. These are the current working version at Cambridge. Every so often I check consistent versions into the SourceForge repository.


MICHAEL J. C. GORDON
University of Cambridge
Computer Laboratory
Room FE19
William Gates Building
JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
work phone: +44 1223 334627
work fax: +44 1223 334678
email: mjcg@cl.cam.ac.uk