The inverse method implements the automata approach for modal satisfiability

Abstract

This paper ties together two distinct strands in automated reasoning: the tableau- and the automata-based approach. It shows that the inverse tableau method can be viewed as an implementation of the automata approach. This is of interest to automated deduction because Voronkov recently showed that the inverse method yields a viable decision procedure for the modal logic K. © Springer-Verlag Berlin Heidelberg 2001.