allow subtheories for prover selection

[tillmo]

For proving, allow the use of subtheories that are in smaller sublogics, if this means that more provers can be selected. Of course, there must be a flag ensuring that disproving or consistency checking results are not valid w.r.t. the whole theory. For the implementation, compute the sublogic of each individual axiom (and unite these with the sublogic of the signature). Group the axioms by sublogic. For each such sublogic, compute the available provers (possibly via comorphism paths). Compute a Pareto front of optimal choices, the conflicting criteria being: as many as axioms as possible, as many available provers as possible.

With this more principled treatment, we can stop the current practice that provers used for CASL pretend to work for sort generation constraints even if they don't.