 The modal soundness and completeness theorems immediately give rise to a decision procedure to check for any modal formula \(A\) whether \(A\) follows from GL or not, by depth-first search through irreflexive transitive trees of bounded depth. Looking at the procedure a bit more precisely, it can be shown that GL is decidable in the computational complexity class PSPACE, like the well-known modal logics K, T and S4. This means that there is a Turing machine that, given a formula \(A\) as input, answers whether \(A\) follows from GL or not; the size of the memory that the Turing machine needs for its computation is only polynomial in the length of \(A\). One can show that the decision problem for GL (again, like the decision problems for K, T and S4) is PSPACE-complete, in the sense that all other problems in PSPACE are no harder than deciding whether a given formula is a theorem of GL. (See Goré and Kelly (2007) for the description of an automated theorem prover for GL.)