1REWRITER(1)                 General Commands Manual                REWRITER(1)
2
3
4

NAME

6       rewriter - demodulate terms
7

SYNOPSIS

9       rewriter <demodulators-file> < <terms-file> > <rewritten-terms-file>
10

DESCRIPTION

12       This manual page documents briefly the rewriter command.
13
14       Rewrite a stream of terms with a list of demodulators. The demodulators
15       are used left-to-right as given, and they are not checked for  termina‐
16       tion.
17

SYNTAX

19       The  file  of  demodulators  contains  optional commands then a list of
20       demodulators.  The commands can be used to declare infix operations and
21       associativity/commutativity.  Example file of demodulators:
22
23           op(400, infix, ^).
24           op(400, infix, v).
25           assoc_comm(^).
26           assoc_comm(v).
27           formulas(demodulators).
28           x ^ x = x.
29           x ^ (x v y) = x.
30           x v x = x.
31           x v (x ^ y) = x.
32           end_of_list.
33
34

SEE ALSO

36       prover9(1), mace4(1).
37       Full  documentation for rewriter is found in the prover9 manual, avail‐
38       able   on   Debian   systems   in   the    prover9-doc    package    at
39       /usr/share/doc/prover9-doc/manual/index.html.
40

AUTHOR

42       rewriter was written by William McCune <mccune@cs.unm.edu>
43
44       This    manual    page    was    written    by    Peter   Collingbourne
45       <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used  by  oth‐
46       ers).
47
48
49
50                               January 20, 2007                    REWRITER(1)