Work on LDS and Tableaux methods was initiated in the EPSRC supported project ADULT (GR/J/14715), 1993-1996. Algorithmic Deduction with Labelled Tableaux (Final report)
Compiled LDS (CLDS) in collaboration with with Dr. Alessandra Russo. goes one step further and employs, in a uniform way, a first order semantics for LDS, so that automation is possible via adaptations of standard theorem provers. So far, the families of modal logics and resource logics,including fuzzy logic, have been fully studied and the results published. (See Krysia Broda, Dov Gabbay, Luis Lamb and Alessandra Russo. Compiled Labelled Deductive Systems: A Uniform Presentation of Non-Classical Logics, Research Studies press, 2004 ISBN 0863802966.)
Other logics for which the approach is applicable include Description Logic, Hybrid Logics, Term Modal Logics and logics based on the ambient calculus. Natural deduction, tableaux methods and refutation theorem provers have been used as the proof method at the first order level, whilst natural deduction and tableaux methods have been used at the CLDS level. See the distinguished MSc dissertation of Aikaterina Marazopoulou (PG 2009) for a formal framework for CLDS using tableau systems.
A slightly different approach, applied to logic and probability, can be found in Bjorn Bjurling's PhD Thesis