### Miscellaneous LADR Applications

Here are examples of running the auxiliary programs described in the MACE4 manual. You can get a synopsis of each program by giving it an argument "`help`".

- Remove isomorphic interpretations. This example produces the quasigroups of order 3.

      mace4 -n3 < qg.in | get_interps > qg.out3
      isofilter < qg.out3 > qg.iso3

- Use a set of interpretations to filter a stream of clauses. This example removes clauses that are true in any of a set of non-modular orthomodular lattices.

      modfilter non-MOL-OML false_in_all < MOL-cand.296 > MOL-cand.238

- Use a set of clauses to filter a stream of interpretations. This example removes distributive models from a set of ortholattices.

      mace4 -n8 < OL.in | get_interps | isofilter > OL.8
      interpfilter distributivity nonmodels < OL.8 > OL.8.out

- Given a set of interpretations and a stream of clauses, show the interpretations that model each clause.

      mace4 -n6 < OL.in | get_interps | isofilter > OL.6
      modtester OL.6 < BA-sheffer > BA-sheffer.out

- Decision procedure for lattice identities in meet/join.

      latfilter < meet-join-equations > meet-join-equations.out

- Decision procedure for ortholattice identities in meet/join/complement/0/1/shefferstroke.

      olfilter < mjc01s-equations > mjc01s-equations.out

- Given a set of rewrite rules (demodulators), rewrite a stream of terms or clauses.

      rewriter lattice.rules < lattice-sax > lattice-sax.rewritten

- Print the upper covers of the 5 ortholattices of order 8. The output is suitable for input to Ralph Freese's lattice drawing program.

      upper-covers < OL.8 > OL.8.upper-covers

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.