clausefilter(1) filter formulas with models

SYNOPSIS

clausefilter <interpretations-file> <test> < <formulas-file> > <passing-formulas-file>

DESCRIPTION

This manual page documents briefly the clausefilter command.

Given a set of interpretations, a test to perform, and a stream of formulas, clausefilter outputs the formulas that pass the test.

TESTS

The following tests are available.
true_in_all
Formula true in all interpretations.
true_in_some
Formula true in some interpretation.
false_in_all
Formula false in all interpretations.
false_in_some
Formula false in some interpretation.

AUTHOR

clausefilter was written by William McCune <[email protected]>

This manual page was written by Peter Collingbourne <[email protected]>, for the Debian project (but may be used by others).