Improve isCong congruence testing

[rzach]

In ml_interactive, the predicate isCong will find all strong congruences of a logic. The way it does that is by listing all partitions of the designated and undesignated truth values and checking if such a partition is a congruence (all operators respect it).

a) I am not perfectly confident the implementation is correct and complete. So testing and inspection is needed.

b) Improve speed, especially the speed with which an optimal (smallest) solution is found: There are two places to look for improvements: cut down on the number of partitions tested (or test better candidates first), and speed up the testing of the individual partitions.

• The predicate partition(List, Partition) does the work of generating partitions. It does so from finest to coarsest (i.e., starts with [[a],[b],[c]] and ends with [[a,b,c]]). Since we're mainly interested in partitions of minimal size it would be nice to replace partition with a predicate that finds partitions with smaller number of classes first.
• Need to think about relation between different congruences. Here's a hunch for instance (although if it's true then isCong definitely is broken because it's not what's showing up in the tests I ran): if there's a congruence in which two designated values are equivalent, then also the corresponding congruence with non-designated values partitioned into singletons is a congruence. So first find the partitions of the designated values (fewer in number if few designated values) where none of the non-designated values are identitifed, then find partitions of the non-designated values only for these.

[rzach]

Better idea: generate partial congruences (i.e., partitions of just n truth values). If a partial partition fails the congruence test (e.g., a,b in same class but ~a, ~b not in same class) then no partition containing this partial partition can be a congruence, so if we fail on this partition, we cut off a large chunk of the search tree (larger, in any case, than just the single partition we eliminate if we naively enumerate every partition and test it). So start with small partitions, fail if it fails the congruence test, then add another element and construct all partial partitions also involving the new element (ie, new element can be a singleton class by itself or be added to any existing class).