A partir de 1960, y debido al desarrollo de las semánticas de Kripke, se establecieron conexiones sencillas entre axiomas de la Lógica Modal y propiedades de la denominada “relación de accesibilidad” entre mundos. La profundización de estos avances desembocó en la formulación de la Teoría de la Correspondencia. Según van Benthem dicha teoría tiene como objeto “el estudio sistemático de la definibilidad clásica de fórmulas modales, consideradas como principios relacionales”. Si bien para algunos axiomas de la Lógica Modal resulta sencillo establecer qué condición debe cumplir la relación de accesibilidad para validarlo, esto no puede generalizarse. Además, se ha establecido que no toda fórmula de la Lógica Modal es definible en Lógica de Predicados de Primer Orden con Identidad (LPOI).
Nuestro trabajo está guiado por el interés en hallar un procedimiento que, aplicado a una fórmula cualquiera de la Lógica Modal Proposicional (LMP) nos dé como resultado la condición que debe cumplir la clase de marcos que la valide.