There are several kinds of tableaus for modal logic. We have been looking at prefixed tableaus. Here are notes about destructive tableaus.
Next, here is a Prolog program that implements a decision procedure for the modal logic K.