.TH CLAUSEFILTER 1 "January 20, 2007"
.SH NAME
clausefilter - filter formulas with models
.SH SYNOPSIS
.B clausefilter
.RI < interpretations-file >
.RI < test >
<
.RI < formulas-file >
>
.RI < passing-formulas-file >
.SH DESCRIPTION
This manual page documents briefly the
.B clausefilter
command.
.PP
Given a set of \fIinterpretations\fP, a \fItest\fP to perform, and a
stream of \fIformulas\fP, \fBclausefilter\fP outputs the formulas
that pass the test.
.SH TESTS
The following tests are available.
.TP
.B true_in_all
Formula true in all interpretations.
.TP
.B true_in_some
Formula true in some interpretation.
.TP
.B false_in_all
Formula false in all interpretations.
.TP
.B false_in_some
Formula false in some interpretation.
.SH SEE ALSO
.BR prover9 (1),
.BR mace4 (1).
.br
Full documentation for \fBclausefilter\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
\fBclausefilter\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).