man pgen (Commandes) - generates single step proof obligations out of a DFG (SPASS) proof

NAME

pgen - generates single step proof obligations out of a DFG (SPASS) proof

SYNOPSIS

pgen [ -dstqjnr] [-vinci -xvcg] filename

OPTIONS

The following options are supported by pgen: Do not generate proof files. Quiet mode. Prefix of generated files. The option name was chosen because the prefix is probably a directory. Number of seconds for each proof attempt for each proof step. Default is 3 seconds. Suffix of files generated by pgen. Default is '.dfg'. Write representation of the reduced tableau to <filename>. Write representation of the non-reduced tableau to <filename>. Write tableau representation in daVinci format. Write tableau representation in xvcg format.

NOTES

VCG is a public domain tool intended for visualizing compiler graphs. It is developed by Georg Sander at the University of Saarbruecken. It is available via anonymous ftp at 

        ftp.cs.uni-sb.de
in the directory pub/graphics/vcg. Or visit 

        http://rw4.cs.uni-sb.de/~sander/html/gsvcg1.html.
daVinci is another public domain graph visualizing tool. Get it at 

        ftp.tzi.de
in the directory /tzi/biss/daVinci. The WWW address is 

        http://www.informatik.uni-bremen.de/daVinci/.

SEE ALSO

checkstat(1), filestat(1), pcs(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)

AUTHORS

Thorsten Engel and Christian Theobalt.

Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de> Christoph Weidenbach <weidenb@mpi-sb.mpg.de>