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.