5. pgen

5.1 NAME

pgen - generates single step proof obligations out of a DFG (SPASS) proof

5.2 SYNOPSIS

pgen [ -dstqjnr] [-vinci -xvcg] filename

5.3 DESCRIPTION

¢ man begin DESCRIPTION pgen is a C-program that checks the tableau structure of SPASS tableau proofs and generates proof tasks corresponding to proof steps. Before the proof tasks are generated, the tableau is reduced in two steps:

1. If an empty clause exists in a subtableau, all successors of the subtableau are deleted.
2. If a subtableau has a single successor subtableau, the successor is deleted.

After the reduction, pgen checks that

• Each clause in a subtableau uses only parents clauses that are visible at this point in the tableau.
• Each clause, except for split clauses, has the maximum split level of its parents.
• If the first half of a split was ground, then negations of its literals can be used in the tableau branch corresponding to the second half of the split.
• The tableau is complete and closed.

Generated filenames have the form <prefix><filename><suffix>, where suffix and prefix are specified by the -d and -s option.

pgen can generate graph representations of the tableau before and after the reduction using the -n and -r options. These representations can be written to a text file in either daVinci or xvcg format. See section See section DAVINCI AND VCG, for these graph visualization programs.

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

5.5 DAVINCI AND VCG

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

5.6 AUTHORS

Thorsten Engel and Christian Theobalt.

Contact : spass@mpi-inf.mpg.de

5.7 SEE ALSO

checkstat(1), filestat(1), pcs(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)

This document was generated by Christoph Weidenbach on February, 23 2010 using texi2html 1.78.