Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів

Thumbnail Image
Касьянюк, Веда
Малютенко, Людмила
Шкільняк, Оксана
Journal Title
Journal ISSN
Volume Title
У статті розглянуто програмно-орієнтовні логічні формалізми – чисті першопорядкові композиційно-номінативні транзиційні модальні логіки немонотонних часткових предикатів. На основі властивостей відношення логічного наслідку для множин специфікованих станами формул для цих логік побудовано числення секвенційного типу. Описано різновиди таких числень, для них доведено теореми коректності та повноти.
Modal logics give tools which help to efficiently solve a variety of problems in informatics and programming. Classical predicate logic is the basis for traditional modal logics. However, classical logic does not allow sufficiently taking into account incompleteness and partiality of information. This leads to a problem of construction of program-oriented logical formalisms. Composition of nominative modal logics could be such a formalism combining capabilities of logics of partial quasi-ary predicates and traditional modal logics. Modal transitional logics (MTL), their important variant, can adequately represent changes and development of subject-domains. Effective reasoning may be a key part of many information and program systems. Sequent calculus is an efficient Gentzen-style deduction system. Sequent calculi are a formalization of logical consequence, one of the central concepts of logic. This paper studies pure first-order MTL of partial quasi-ary predicates without monotonicity restriction and construct sequent calculi for them. We define multimodal, temporal and general MTL. It is sufficient to consider only general MTL (GTL); obtained results can be carried to multimodal and temporal MTL. We describe languages and semantic models of pure first-order MTL and logical consequence relations for sets of specified with state names formulae. Basing on properties of the defined relations, we construct sequent calculi for GTL of non-monotone predicates. Their distinctive features include extended conditions for sequent closure, new sequent forms for elimination of modalities and forms for quantifier elimination respecting non-monotonicity. Depending on restrictions imposed on the transition relation, various classes of GTL can be introduced. We consider most conventional cases: the relation can be reflexive, symmetric, or transitive (or their combination). This leads to a number of different sequent forms for modalities elimination, and correspondingly, of different variants of sequent calculi. For the specified calculi, we describe a derivation procedure and prove the soundness and completeness theorems.
модальна логіка, предикат, логічний наслідок, секвенційне числення, modal logic, predicate, sequent calculus, logical consequence
Касьянюк Веда Станіславівна. Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів / Касьянюк В. С., Малютенко Л. М., Шкільняк О. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 23-29.