[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

5. pgen


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

5.1 NAME

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


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

5.2 SYNOPSIS

pgen [ -dstqjnr] [-vinci -xvcg] filename
[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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:
  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

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.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

5.6 AUTHORS

Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

5.7 SEE ALSO

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


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Renate Schmidt on March, 10 2003 using texi2html