The global properties of valid formulas in modal logic K

Global property is the necessary condition which must be satisfied by the provable formulas. It can help to find out some unprovable formula that does not satisfy some global property before proving it using formal automated reasoning systems, thus the efficiency of the whole system is improved. This paper presents some global properties of valid formulas in modal logic K. Such properties are structure characters of formulas, so they are simple and easy to check. At the same time, some global properties of K unsatisfiable formula set are also given.