---
name: "pgen"
section: "1"
platform: "linux"
package: "spass"
version: "2.1-4"
release: "Debian 5.0 (Lenny)"
platforms: ["linux"]
url: "https://new.carta.tech/pgen"
---

# pgen(1)

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

## NAME

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

## SYNOPSIS

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

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

## SEE ALSO

*checkstat*(1), *filestat*(1), [*pcs*(1)](/pcs/1.md), *rescmp*(1), *tpform*(1), *tpget*(1), *deprose*(1), [*dfg2otter*(1)](/dfg2otter/1.md), *dfg2otterpl*(1), [*SPASS*(1)](/SPASS/1.md)

## AUTHORS

Thorsten Engel and Christian Theobalt.

Contact : Thomas Hillenbrand \<hillen@mpi-sb.mpg.de\>\
           Christoph Weidenbach \<weidenb@mpi-sb.mpg.de\>