A general proof method for first-order modal logic
Peter E. Jackson, Han Reichgelt · 1987
We present a general sequent-based proof method for first-order modal logics in which the Barcan formula holds. The most important feature of our system is the fact that it has identical inference rules for every modal logic; different modal logics can be obtained by changing the conditions under which two formulas are allowed to resolve against each other It is argued that the proof method is very natural because these conditions correspond to the conditions on the accessibility relation in Kripke semantics. I