prove: Theorem Proving

$next$ $up$ $previous$ $contents$
Next: rp: Displaying Proofs Up: Saturate Commands Previous: prec: Precedence Definition Contents

`prove`: Theorem Proving

$\begin{displaymath} \mbox{{\tt prove($F$)}} \end{displaymath}$

invokes a theorem proving process for

by negating

and saturating $\neg F$ . The general form of prove is

$\begin{displaymath} \mbox{{\tt prove($F,L,M,O$)}} \end{displaymath}$

for proving

in logic

with translation option

and Saturate options

and

are as for the function translate.

is a list of sa flag settings or option settings.

Harald Ganzinger 2002-12-04