- Otter
-
searches for proofs. For example,
otter < OML1.in > OML1.out
- Mace
-
searches for models or counterexamples. There are two separate programs:
- Mace2 accepts the same inputs as Otter (well, almost).
- Mace4 is usually better for equational problems.
Examples:
mace2 -N6 -p < nonmod-OL2.in > nonmod-OL2.out
mace4 -N6 < nonmod-OL4.in > nonmod-OL4.out
- modfilter
-
This C program takes a set of interpretations (as a
filename argument) and uses it to filter a stream of clauses (on stdin).
Clauses that pass the filter are sent to stdout. The type of filter is
the second argument:
true_in_all, true_in_some, false_in_all,
or false_in_some.
An optional third argument "fast" tells modfilter to expect clauses in
"fastparse" form. Examples:
modfilter non-MOL-OML false_in_all fast < MOL-cand.296.fast > MOL-cand.238.fast
modfilter non-MOL-OML false_in_all < MOL-cand.296 > MOL-cand.238
- isofilter
-
This C program takes a stream of interpretations (from stdin)
and eliminates the isomorphic ones. The interpretations are
in Mace4's "print_models_portable" form. Isofilter is
typically used with Mace4, because Mace4 usually produces
lots of isomorphic models. In the following example,
Mace4 is asked to generate all the ortholattices of size 10;
it produces 1247 of them, and isofilter says that only 15
those are nonisomorphic.
mace4 -n10 < OL.in | get_interps | isofilter > OL.10
Isofilter does not (although maybe it should) check for
isomorphism by renaming operations (e.g., dual lattices
are not necessarily isomorphic). It simply checks
relevant permutations of the domain elements.
- olfilter
-
This C program takes a stream of equations (from stdin)
and passes the ortholattice identities through to stdout.
It implements Brun's extension of the Whitman decision procedure
for lattice identities. An optional argument "fast" tells the
program to expect equations in "fastparse" form. Examples:
olfilter fast < ol.in.fast > ol.out.fast
olfilter < ol.in > ol.out
Unfortunately, olfilter is very rigid and inconsistent about
the symbols it accepts.
In fastparse form it accepts [=,m,j,c,f,0,1,variables].
In ordinary form it accepts [=,^,v,c,f,0,1,variables].
If an input equation is in terms of meet and join only,
olfilter functions as a Whitman procedure for LT,
because OL is a conservative extension of LT.
- unfast
-
This simple C program takes a stream (from stdin) of clauses in
fastparse form, and writes them (on stdout) in ordinary form.
Example:
unfast < MOL-cand.296.fast > MOL-cand.296
- ploop3
-
This perl program runs a sequence of Otter jobs.
A common Otter input file (the first argument) is used for all of the jobs,
and a stream of clauses is input. For each clause C on stdin,
C is appended to the sos list, and Otter is called.
Only a few bits of Otter's output (e.g., proof messages) are sent to
the output of ploop3.
The following example shows that each of 238 candidates is a MOL identity.
ploop3 head < 238-denials > 238-denials.out
- frogmen5b
-
This C program generates well-formed equations alpha = x, where alpha
is a binary term whose leaves are variables.
It takes three arguments:
- assoc: the structure of alpha
- ops: the sequence of (binary) operations in alpha
- args: the sequence of variables in alpha
The program simply generates all combinations of those three sets.
The following example generates the length-9 equations of interest.
frogmen5b assoc-11 ops-11 args-11 > frog-11.out
In practice, because frogmen generates great numbers of equations, the
output is piped directly to a filter, for example,
frogmen5b assoc-13 ops-13 args-13 | olfilter fast > cand-13.out
- go-27B
-
This is a shell script that strings together many of the programs
described on this page.
It generates equations, filters them through various interpretations,
and calls Otter (via ploop3) on the surviving candidates.