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:
"−j"
Do not generate proof files.
"−q"
Quiet mode.
"−d prefix"
Prefix of generated files. The option name was chosen because the prefix is probably a directory.
"−t limit"
Number of seconds for each proof attempt for each proof step. Default is 3 seconds.
"−s suffix"
Suffix of files generated by pgen. Default is ’.dfg’.
"−r filename"
Write representation of the reduced tableau to <filename>.
"−n filename"
Write representation of the non-reduced tableau to <filename>.
"−vinci"
Write tableau representation in daVinci format.
"−xvcg"
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>