TABLEAUX, 1997 Bernhard Beckert and Rajeev Gore Free Variable Tableaux for Propositional Modal Logics We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain "free" and "universal" variables. Our "lean" Prolog implementation is not only surprisingly short, but compares favourably with other considerably more complex implementations for modal deduction.