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 <[email protected]>
Christoph Weidenbach <[email protected]>