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

Loading...
Thumbnail Image
Date
2016
Authors
Нікітченко, Микола
Шкільняк, Степан
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Запропоновано новий клас програмно-орієнтованих логічних формалізмів – чисті першопорядкові логіки із квазіарними та n-арними предикатами. Такі формалізми є синтезом класичних першопорядкових логік і композиційно-номінативних логік квазіарних предикатів. Розглянуто семантичні моделі та мови і досліджено семантичні властивості пропонованих логік. Встановлено зв’язок між n-арними та X-арними предикатами, описано нормальні форми. Досліджено відношення логічного наслідку, наведено властивості цих відношень для арних атомарних формул.
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.
Keywords
логіка, квазіарний предикат, n-арний предикат, логічний наслідок, logic, quasiary predicate, n-ary predicate, logical consequence
Citation
Нікітченко Микола Степанович. Першопорядкові логіки із квазіарними та n-арними предикатами / Нікітченко М. С., Шкільняк С. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 16-22.