Isofilter

If Mace4 produces more than one structure, some of them are very likely to be isomorphic to others. The program Isofilter can be used to remove isomorphic structures.

Determining whether two structures are isomorphic is a hard problem in general, but isofilter can cope with some large structures in reasonable time. It depends on the type of the strucure. For example, quasigroups usually take more time than lattices.

Isofilter accepts structures in LADR standard format, which is the default format produced by Mace4. However, the Mace4 output contains a lot of extraneous information, which can be stripped out with the command interpformat standard. Isofilter also accepts the following command-line arguments, which are described in the examples below.

ignore_constants: ignore all constants during the isomorphism tests.
check '<operations>' : consider only the listed operations in the isomorphism tests.
output '<operations>' : output only the listed operations.
wrap: enclose the resulting structures in list(interpretations). ... end_of_list.

Examples

We start with a Mace4 job and extract the interpretations; then we run Isofilter.

mace4 -N6 -m -1 -f BA2.in | interpformat standard > BA2.interps 
isofilter < BA2.interps > BA2.interps2

Note that the two models in BA2.interps2 differ only in one of the constants. In this case the constants come from existentially quantified variables in the goal, and all we really care about is the lattice. We can tell Isofilter to ignore differences in constants by giving it the argument ignore_constants as in the following command.

isofilter ignore_constants < BA2.interps > BA2.interps3

Another way to use only a subset of the operations is the check argument, which us used to specify exactly which operations to test for isomorphism. In the following example, only the meet and join operations are checked. (If there is more than one operation, or if the operation may be interpreted by the shell, they should be enclosed in single quotes.)

mace4 -N6 -m -1 -f MOL.in | interpformat standard > MOL.interps 
isofilter check '^ v' output '^ v' < MOL.interps > MOL.interps2

The output of isofilter is frequently used as input to a program that expects the interpretations to be in a list of interpretations; we can tell isofilter to put the output in that form by giving it the argument wrap as in the following command.

isofilter ignore_constants wrap < BA2.interps > BA2.interps4

Finally, we can string together some of the preceding commands as follows.

mace4 -N6 -m -1 -f BA2.in | interpformat standard | isofilter ignore_constants wrap > BA2.interps5

Next Section: Prooftrans