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

Show simple item record

dc.contributor.author Касьянюк, Веда
dc.contributor.author Малютенко, Людмила
dc.contributor.author Шкільняк, Оксана
dc.date.accessioned 2017-03-13T12:52:26Z
dc.date.available 2017-03-13T12:52:26Z
dc.date.issued 2016
dc.identifier.citation Касьянюк Веда Станіславівна. Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів / Касьянюк В. С., Малютенко Л. М., Шкільняк О. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 23-29. uk_UA
dc.identifier.uri http://ekmair.ukma.edu.ua/handle/123456789/11115
dc.description 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. en_US
dc.description.abstract У статті розглянуто програмно-орієнтовні логічні формалізми – чисті першопорядкові композиційно-номінативні транзиційні модальні логіки немонотонних часткових предикатів. На основі властивостей відношення логічного наслідку для множин специфікованих станами формул для цих логік побудовано числення секвенційного типу. Описано різновиди таких числень, для них доведено теореми коректності та повноти. uk_UA
dc.language.iso uk uk_UA
dc.subject модальна логіка uk_UA
dc.subject предикат uk_UA
dc.subject логічний наслідок uk_UA
dc.subject секвенційне числення uk_UA
dc.subject modal logic en_US
dc.subject predicate en_US
dc.subject sequent calculus en_US
dc.subject logical consequence en_US
dc.title Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів uk_UA
dc.title.alternative Sequent Calculi of Composition of Nominative Modal Logics of Non-Monotone Predicates en_US
dc.type Article uk_UA
dc.status published earlier uk_UA
dc.relation.source Наукові записки НаУКМА: Комп'ютерні науки uk_UA

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search DSpace


My Account