  Known realization algorithms which recover evidence terms in modal  theorems use cut-free derivations in the corresponding modal logics.  Alternatively, the Realization Theorem can be established  semantically by Fitting’s method or its proper modifications.  In principle, these semantic arguments also produce  realization procedures which are based on exhaustive search.