pgen(1)
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>