Flit DAG dumper for Twelf 1.4 Copyright (C) 2002 Roberto Virga. All rights reserved. N.B. The following instructions assume the availability of the flit binary program and related tools, as maintained in the Foundational Proof-Carrying Code project at Princeton. (For further information, see .) To use: The DAG dumper functions only inside twelf-sml, and it is not currently accessible from twelf-server. First you need to initialize the dumper, by typing: Flit.init ; where is the path (either absolute, or relative to the current working directory) to the TCB symbol table file generated using the files in logic/pcc/flit/untrusted. After you have initialized the dumper by providing the symbol table of the TCB as outlined above, there are two ways you can use the dumper: a) to dump a single symbol (together with all the other non-TCB symbols it might depend): Flit.dump ; b) to dump all symbols used in a logic program: Flit.setFlag (); Twelf.Config.append (Twelf.Config.read ); Flit.dumpFlagged ; will dump all symbols loaded since Flit.setFlag () was issued, and in particular, all symbols introduced by loading the Twelf configuration file . All such symbols will have the "clause" bit set to 1 (the clause bit is the 10th bit of the first field of a node, and can be retrieved by doing a logical and with mask 512).