pgen

Langue: en

Version: 2003-04-29 (debian - 07/07/09)

Section: 1 (Commandes utilisateur)

Sommaire

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>