OLSAX Programs

Back to the Main Page
searches for proofs. For example,
    otter < OML1.in > OML1.out 
searches for models or counterexamples. There are two separate programs: Examples:
    mace2 -N6 -p < nonmod-OL2.in > nonmod-OL2.out 
    mace4 -N6    < nonmod-OL4.in > nonmod-OL4.out 

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 
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.

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.

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
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
This C program generates well-formed equations alpha = x, where alpha is a binary term whose leaves are variables. It takes three arguments: 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
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.