Modal logics of partial quasiary pradicates with equality and sequent calculi of this logics

The aim of the work is to study new classes of program-oriented logical formalisms of the modal type – pure first-order modal logics of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Modal logics can be used to describe and model various subject areas, artificial intelligence systems, information and software systems. The limitations of the classical predicate logic on which traditional modal logics are based determine the relevance of the problem of introducing new program-oriented logical formalisms. Such are composition-nominative modal logics, which synthesize facilities of traditional modal logics and logics of partial quasiary predicates. One of their important classes are transitional modal logics (TML), they reflect the aspect of change and evolution of subject areas. We denote pure first-order TML by TMLQ. In this paper two types of TMLQ with equality are considered: TMLQ (with strong equality predicates xy), and TMLQ= (with weak equality predicates =xy). For quantifier elimination in logics of non-monotonic predicates special predicates which indicate whether a component with a corresponding name has a value in the input data are required. The use of these predicates is a characteristic feature of both TMLQ and TMLQ=. Total indicator predicates determine the presence or absence of a component with a certain name, while partial indicator predicates signalize only the presence of such a component. Thus, total indicator predicates are introduced as special parametric 0-ary compositions Ez in TMLQ, and partial indicator predicates are represented in TMLQ= as predicates =xx. Another feature of TMLQ and TMLQ= is the use of the extended renomination compositions. In this paper we describe semantic models and languages of TMLQ and TMLQ=. Particular attention is paid to the properties related to equality predicates, substitution of equals in TMLQ and TMLQ= is described. A number of logical consequence relations for these logics are defined on sets of formulas specified with states. On this semantic basis, the corresponding sequent type calculi are proposed for the investigated logics.