tableaux. Nobody seems care about making sequent type or Hilbert type calculus for DL things. The problem you've put forward would require such calculi (either we think of graphical or non-graphical rendering of axioms andconsequences). Should we then try to create one? Perhaps it would be a peace of cake(?) serguei