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
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:
-
If an empty clause exists in a subtableau, all
successors of the subtableau are deleted.
-
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 5.5 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
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
in the directory /tzi/biss/daVinci. The WWW address is
| http://www.informatik.uni-bremen.de/daVinci/.
|
5.6 AUTHORS
Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.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 Renate Schmidt on March, 10 2003
using texi2html