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/gsvc.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>