Першопорядкові логіки із квазіарними та n-арними предикатами
Loading...
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.