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

NAME

6       clausefilter - filter formulas with models
7

SYNOPSIS

9       clausefilter  <interpretations-file>  <test> < <formulas-file> > <pass‐
10       ing-formulas-file>
11

DESCRIPTION

13       This manual page documents briefly the clausefilter command.
14
15       Given a set of interpretations, a test to perform, and a stream of for‐
16       mulas, clausefilter outputs the formulas that pass the test.
17

TESTS

19       The following tests are available.
20
21       true_in_all
22              Formula true in all interpretations.
23
24       true_in_some
25              Formula true in some interpretation.
26
27       false_in_all
28              Formula false in all interpretations.
29
30       false_in_some
31              Formula false in some interpretation.
32

SEE ALSO

34       prover9(1), mace4(1).
35       Full  documentation  for  clausefilter  is found in the prover9 manual,
36       available  on  Debian   systems   in   the   prover9-doc   package   at
37       /usr/share/doc/prover9-doc/manual/index.html.
38

AUTHOR

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