Першопорядкові логіки із квазіарними та n-арними предикатами

Show simple item record

dc.contributor.author Нікітченко, Микола
dc.contributor.author Шкільняк, Степан
dc.date.accessioned 2017-03-13T12:58:55Z
dc.date.available 2017-03-13T12:58:55Z
dc.date.issued 2016
dc.identifier.citation Нікітченко Микола Степанович. Першопорядкові логіки із квазіарними та n-арними предикатами / Нікітченко М. С., Шкільняк С. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 16-22. uk
dc.identifier.uri http://ekmair.ukma.edu.ua/handle/123456789/11116
dc.description Verification is one of the important methods of improving the reliability of software. It should be based on logics that adequately reflect the main properties of programs. Among such properties are partiality and nondeterminism of programs, usage of complex data structures, etc. In particular, programs use mapping of fixed arity (n-ary mappings) and of flexible arity (quasiary mappings). These properties imply the necessity of construction of program-oriented logics that are based on n-ary and quasiary mapping. This paper considers one of these logics – pure first-order logic of quasiary and n-ary predicates. This logic is a synthesis of firstorder classical logic and first-order composition-nominative logics of quasiary predicates. As semantic models, quasiary predicate algebras and their subalgebras of various types are considered, in particular, subalgebras of equitone and X-ary predicates. The class of compositions consists of compositions of disjunction, negation, renomination, and existential quantification. Semantic properties of algebras with these compositions are studied. The connection between n-ary and X-ary predicates is described. Based on algebras with these compositions, a logic language is defined as the set of terms of corresponding algebras. This language being restricted by the class of n-ary predicate symbols coincides with the first-order language of classical logic; and being restricted by the class of quasiary predicate symbols it coincides with the language of firstorder quasiary logic. The paper describes the following types of logical consequences: irrefutability consequence |=IR, consequence on truth |=T, consequence on falsity |=F, and a strong consequence on truth and falsity |=TF. Semantic properties of these consequences are investigated. In particular, logical equivalence relations are studied for the introduced consequences. Transformations based on such equivalence relations permit to transform formulas to various normal forms. The formulated semantic properties form the basis for sequent rules and corresponding sequent calculi for the defined logics. en
dc.description.abstract Запропоновано новий клас програмно-орієнтованих логічних формалізмів – чисті першопорядкові логіки із квазіарними та n-арними предикатами. Такі формалізми є синтезом класичних першопорядкових логік і композиційно-номінативних логік квазіарних предикатів. Розглянуто семантичні моделі та мови і досліджено семантичні властивості пропонованих логік. Встановлено зв’язок між n-арними та X-арними предикатами, описано нормальні форми. Досліджено відношення логічного наслідку, наведено властивості цих відношень для арних атомарних формул. uk
dc.language.iso uk uk
dc.subject логіка uk
dc.subject квазіарний предикат uk
dc.subject n-арний предикат uk
dc.subject логічний наслідок uk
dc.subject logic uk
dc.subject quasiary predicate en
dc.subject n-ary predicate en
dc.subject logical consequence en
dc.title Першопорядкові логіки із квазіарними та n-арними предикатами en
dc.title.alternative First-Order Logics with Quasi-Ary and N-Ary Predicates uk
dc.type Article uk
dc.status published earlier uk
dc.relation.source Наукові записки НаУКМА: Комп'ютерні науки uk

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search DSpace


My Account