.de Sp \" Vertical space (when we can't use .PP)
.if t .sp .5v
.if n .sp
..
.de Vb \" Begin verbatim text
.ft CW
.nf
.ne \\$1
..
.de Ve \" End verbatim text
.ft R
.fi
..
.TH REWRITER 1 "January 20, 2007"
.SH NAME
rewriter - demodulate terms
.SH SYNOPSIS
.B rewriter
.RI < demodulators-file >
<
.RI < terms-file >
>
.RI < rewritten-terms-file >
.SH DESCRIPTION
This manual page documents briefly the
.B rewriter
command.
.PP
Rewrite a stream of \fIterms\fP with a list of \fIdemodulators\fP. The
demodulators are used left-to-right as given, and they are not checked
for termination.
.SH SYNTAX
The file of demodulators contains optional commands
then a list of demodulators.  The commands can be used to
declare infix operations and associativity/commutativity.
Example file of demodulators:
.Sp
.Vb 10
\&    op(400, infix, ^).
\&    op(400, infix, v).
\&    assoc_comm(^).
\&    assoc_comm(v).
\&    formulas(demodulators).
\&    x ^ x = x.
\&    x ^ (x v y) = x.
\&    x v x = x.
\&    x v (x ^ y) = x.
\&    end_of_list.
.Ve
.Sp
.SH SEE ALSO
.BR prover9 (1),
.BR mace4 (1).
.br
Full documentation for \fBrewriter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
.SH AUTHOR
\fBrewriter\fP was written by William McCune <mccune@cs.unm.edu>
.PP
This manual page was written by Peter Collingbourne <peter@pcc.me.uk>,
for the Debian project (but may be used by others).