pgen1

Usage

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