SIXTEEN gives not complete error

[rzach]

Trying to put in the Shramko-Wansing logic based on the ordering but

ordering(truth,"{nf < f, nf < n, nf < nfb, nf < nft, f < fb, f < ft, f < e, n < e, n < nb, n < nt, nfb < fb, nfb < a, nf < nb, nft < ft, nft < a, nft < nt, fb < ftb, fb < b, ft < ftb, ft < t, nb < b, nb < ntb, nt < t, nt < ntb, b < tb, t < tb, a < ftb, a < ntb, ftb < tb, ntb < tb }"). 

gives error

*** Error in ordering 'truth': Neither complete for 'inf' nor for 'sup'.

(e is the non-italic N in the diagram.)

[gsalzer]

Can you try with nf < nb replaced by nfb < nb? Moreover, e < b and e < t seems to be missing.

[gsalzer]

It should also work to specify the ordering more compactly as

nf < {
   f < {
      fb < {ftb < tb, b < tb},
      ft < {ftb, t < tb},
      e  < {b,t}
   },
   nfb < {
      fb,
      a  < {ftb, ntb},
      nb < {b, ntb}
   },
   nft < {
      ft,
      a,
      nt < {t, ntb < tb}
   },
   n < {e, nb, nt}
}

[rzach]

Neither of these worked :(

ordering(truth,"{nf < f, nf < n, nf < nfb, nf < nft, f < fb, f < ft, f < e, n < e, n < nb, n < nt, e < b, e < t, nfb < fb, nfb < a, nfb < nb, nft < ft, nft < a, nft < nt, fb < ftb, fb < b, ft < ftb, ft < t, nb < b, nb < ntb, nt < t, nt < ntb, b < tb, t < tb, a < ftb, a < ntb, ftb < tb, ntb < tb }"). 

ordering(truth, "nf < { f < { fb < {ftb < tb, b < tb}, ft < {ftb, t < tb}, e  < {b,t} }, nfb < { fb, a  < {ftb, ntb},       nb < {b, ntb} }, nft < { fb, a, nt < {t, ntb < tb} }, n < {e, nb, nt}}").

[rzach]

The compact ordering didn't work, but the explict one does. Only takes an hour to compute the and operator ;) Close unless you feel like figuring out if it's a problem with the compact representation, or with the code.

[gsalzer]

The compact ordering contained a typo, therefore I edited my most yesterday (click on "edited" in my post and select the change to see the difference). With this change, the two input methods specify the same internal ordering, as I checked. Getting the specification of a complex ordering right may indeed be a problem. Regarding long computation times: This could be improved by employing an external program for minimization that is written in a compiled, imperative language. Maybe another enhancement wish ... I doubt that substantial improvements can be made in the Prolog version.

[rzach]

An intermediate solution would be tow write the internal representation of the rules (ie the CNFs) to a file. Then if such a file is present the script could ask if it should be used in generating the .tex file or if it should be regenerated. That way you can run the optimization on a given set of truth values & operators just once. Maybe such a file can then also be used for multseq and we can use them together: multlog to generate the CNFs and then multseq to prove things.

[rzach]

Can Prolog files have long strings broken across lines in the source file?

[rzach]

Nvm found it, \c

[rzach]

Hm no that doesn't do it, I guess Mutlog would have to deal with \c like it does with whitespace? Anyway, yes, the compact version works too so closing this now.

[gsalzer]

I have just pushed a patch that makes MUltlog cache the result of minimizations.