Rechercher une page de manuel
pgen
Langue: en
Version: 2003-04-29 (debian - 07/07/09)
Section: 1 (Commandes utilisateur)
NAME
pgen - generates single step proof obligations out of a DFG (SPASS) proofSYNOPSIS
pgen [ -dstqjnr] [-vinci -xvcg] filenameOPTIONS
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 atftp.cs.uni-sb.dein 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.dein 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>
Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre