Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів
Loading...
Date
2016
Authors
Касьянюк, Веда
Малютенко, Людмила
Шкільняк, Оксана
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
У статті розглянуто програмно-орієнтовні логічні формалізми – чисті першопорядкові композиційно-номінативні транзиційні модальні логіки немонотонних часткових предикатів. На основі властивостей відношення логічного наслідку для множин специфікованих станами формул для цих логік
побудовано числення секвенційного типу. Описано різновиди таких числень, для них доведено теореми
коректності та повноти.
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.
Keywords
модальна логіка, предикат, логічний наслідок, секвенційне числення, modal logic, predicate, sequent calculus, logical consequence
Citation
Касьянюк Веда Станіславівна. Cеквенційні числення композиційно-номінативних модальних логік немонотонних предикатів / Касьянюк В. С., Малютенко Л. М., Шкільняк О. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 23-29.