  In certain substructural logics, such as linear logic and the Lambek calculus, and in the fragment of the relevant logic \(\mathbf{R}\) without disjunction, a Gentzen system can be used to show that the logic is decidable, in that an algorithm can be found to determine whether or not an argument \(X \vdash A\) is valid. This is done by searching for proofs of \(X \vdash A\) in a Gentzen system. Since premises of this conclusion must feature no language not in this conclusion, and they have no greater complexity (in these systems), there are only a finite number of possible premises. An algorithm can check if these satisfy the rules of the system, and proceed to look for premises for these, or to quit if we hit an axiom. In this way, decidability of some substructural logics is assured.