Konrad Slind wrote: > That work was done in the late 1980s. It may be that > Brian Graham still has the proof scripts available. However, > it would probably be very difficult to build a version of HOL > that would run the scripts as-is.
Mike Gordon connected me off-list to Brian Graham and it turned out that the whole formalisation is part of the hol88-contrib-source Ubuntu package. I have not tried yet but in theory it works as the original HOL prover was ported to GNU Common Lisp by Camm Maguire: https://launchpad.net/ubuntu/+source/hol88 > An interesting project would > be to re-do the theories using up-to-date technology. This is my aim as a starting point, not necessarily the whole but the crucial part of it. - Gergely ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/NeoTech _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
