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

NAME

6       interpfilter - filter models with formulas
7

SYNOPSIS

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

DESCRIPTION

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

TESTS

19       The following tests are available.
20
21       all_true
22              All formulas true in given interpretation.
23
24       some_true
25              Some formula true in given interpretation.
26
27       all_false
28              All formulas false in given interpretation.
29
30       some_false
31              Some formula false in given interpretation.
32

SEE ALSO

34       prover9(1), mace4(1).
35       Full  documentation  for  interpfilter  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       interpfilter 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                INTERPFILTER(1)