---
name: "prooftrans"
section: "1"
platform: "linux"
package: "prover9"
version: "0.0.200911a-2.1+b2"
release: "Debian 10 (Buster)"
platforms: ["linux"]
url: "https://new.carta.tech/prooftrans"
---

# prooftrans(1)

tool for transforming Prover9 proofs

## NAME

prooftrans - tool for transforming Prover9 proofs

## SYNOPSIS

**prooftrans** \[*parents\_only*\] \[*expand*\] \[*renumber*\] \[*striplabels*\] \[*-f file*\]\
 **prooftrans** xml \[*expand*\] \[*renumber*\] \[*striplabels*\] \[*-f file*\]\
 **prooftrans** ivy \[*renumber*\] \[*-f file*\]\
 **prooftrans** hints \[*-label label*\] \[*expand*\] \[*striplabels*\] \[*-f file*\]\
 **prooftrans** tagged \[*-f file*\]

## DESCRIPTION

This manual page documents briefly the **prooftrans** command.

**prooftrans** can extract proofs from [**prover9**(1)](/prover9/1.md) output files and transform them in various ways.

## OPTIONS

A summary of options is included below.

- **renumber**

  Renumber steps.

- **parents\_only**

  Simplify justifications by listing only parents.

- **expand**

  Expand all steps, turning secondary justifications into explicit steps.

- **xml**

  Produce proofs in XML.

- **ivy**

  Produce proofs for checking by the IVY proof checker.

- **hints**

  Produce hints for guiding subsequent searches.

- **tagged**

  Produce proofs in a structured tagged format.

- **-label *label***

  Attach label attributes to the hint clauses consisting of the string *label* and a sequence number generated by prooftrans.

- **-f *file***

  Take input from *file* instead of from standard input.

## SEE ALSO

[**prover9**(1)](/prover9/1.md).\
 Full documentation for **prooftrans** is found in the **prover9** manual, available on Debian systems in the *prover9-doc* package at */usr/share/doc/prover9-doc/manual/index.html*.

## AUTHOR

**prooftrans** was written by William McCune \<mccune@cs.unm.edu\>

This manual page was written by Peter Collingbourne \<peter@pcc.me.uk\>, for the Debian project (but may be used by others).