Out of Sorts (Page 2)Really Advanced Topics

To the right of this page you will see a single-sorted version of the problem above. If you hit SOLVE, you may notice that the solver is faster with sort information than without.

The change to be made in the “Sorts” box is obvious: delete everything that is in there and declare just the one generic sort, thing. Then either combine all the enumerations into one long list, as has been done here, or else declare all the names in the “Vocabulary” box and add constraints saying that they are all different from each other, etc.

The key move is to replace each sort expression by a new predicate, so in the “Vocabulary” box, we add:

predicate beast(thing).

and similarly for the predicates day and statement.

Now in the “Constraints” box we should add some formulae identifying the beasts, days and statements, so add a constraint saying that that the beasts are just the lion and the unicorn:

∀ x (beast(x) = (x=lion ∨ x=unicorn)).

and similarly for the days of the week and the statements. Note the form of these constraints: we need to specify not only that the lion is a beast, but also that Monday is not a beast, etc.

The order of days of the week is important. Since we have made them part of the enumeration, we have that for free.

Finally, each variable must be restricted to range over the right things. For example, in the second clause defining “daybefore” we add an antecedent saying that d is a day:

∀ d ((day(d) ∧ d > Monday) → daybefore(d) = PRED(d)).

The reason is that now everything is just a “thing”, meaning we don’t have a clear separation between beasts and days, so we have to beware of what might happen if in a model the lion is greater than Monday!

That’s all! I hope you take away two lessons from this: firstly, elimination of sorts is always possible in principle; secondly, like many things that are possible in principle, it is not generally a good idea!