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

О.S. Shkilniak, S.S. Shkilniak

Abstract


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.

Prombles in programming 2024; 2-3: 19-27


Keywords


modal logic; predicate; logical consequence; sequent calculus

References


S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (eds), Handbook of

Logic in Computer Science, Vol. 1–5, Oxford University Press, 1993 -2000.

D. Bjorner, M.C. Henson (eds), Logics of Specification Languages, EATCS Series, Monograph in Theoretical Computer Sciens, Springer, 2008.

V. Goranko, Temporal Logics, Cambridge University Press, 2023.

F. Kröger, S. Merz. Temporal logic and state systems, Springer Science & Business Media, 2008.

M. Nikitchenko, O. Shkilniak, S. Shkilniak, Pure first-order logics of quasiary predicates, in Problems in Progamming, 2016, No 2–3. pp. 73–86.

S. Shkilniak, First-order composition nominative logics with predicates of weak equality and of strong equality, in Problems in Progamming, 2019, No 3, pp. 28–44.

O. Shkilniak, S. Shkilniak. First-Order Sequent Calculi of Logics of Quasiary Predicates with Extended Renominations and Equality, UkrPROG'2022, CEUR Workshop Proceedings (CEUR-WS.org), 2023, pp. 3–18.

M. Nikitchenko, O. Shkilniak, S. Shkilniak, Sequent calculi of first order logics of partial predicates with extended renominations and composition of predicate complement, in Problems in Progamming, 2020, No 2–3, pp. 182–197.

O. Shkilniak, Modal logics of nonmonotone partial predicates, in Bulletin of Taras Shevchenko National University of Kyiv, Series Physics & Mathematics, 2015, 3, pp. 141–147.

O. Shkilniak, Transitional modal logics of non-monotone quasiary predicates, in Computer Mathematics, 2014, 2, pp. 99–110.


Refbacks

  • There are currently no refbacks.