rp: Displaying Proofs

$next$ $up$ $previous$ $contents$
Next: sat: Starting Saturation Up: Saturate Commands Previous: prove: Theorem Proving Contents

`rp`: Displaying Proofs

$\begin{displaymath} \mbox{{\tt rp, rp($N$)}} \end{displaymath}$

Displays the proof of clause

. If no argument is provided, the proof of the empty clause is printed. Fails, if the specified clause does not exist (anymore).

Harald Ganzinger 2002-12-04