On Some Problems of Efficient Inference Search in First-Order Cut-Free Modal Sequent Calculi

A unified approach is developed for constructing first-order cut-free sequent calculi without equality representing two classes of modal logics in dependence of whether classical logic or intuitionistic one is taken as a basis. It uses the original notions of admissibility and compatibility, which, in general, permits to avoid skolemization being a forbidden operation for the logics under consideration.Additionally, it requires the modal sequent calculi to satisfy a so-called principle-subformula condition. Following the approach, cut-free sequent modal calculi avoiding the dependence of inference search on different orders of quantifier rules applications are described. Results relating to the co-extensivity of various modal sequent calculi are given. The research gives a possibility to construct sound and complete methods for enough high efficient inference search in certain first-order modal logics if efficient technique for the handling of their propositional parts is available.