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.