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

# rewriter(1)

demodulate terms

## NAME

rewriter - demodulate terms

## SYNOPSIS

**rewriter** \<*demodulators-file*\> \< \<*terms-file*\> \> \<*rewritten-terms-file*\>

## DESCRIPTION

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

Rewrite a stream of *terms* with a list of *demodulators*. The demodulators are used left-to-right as given, and they are not checked for termination.

## 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:

```
    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.
```

## SEE ALSO

[**prover9**(1)](/prover9/1.md), [**mace4**(1)](/mace4/1.md).\
 Full documentation for **rewriter** 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

**rewriter** 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).