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

dc.contributor.authorНікітченко, Микола
dc.contributor.authorШкільняк, Степан
dc.date.accessioned2017-03-13T12:58:55Z
dc.date.available2017-03-13T12:58:55Z
dc.date.issued2016
dc.descriptionVerification 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.identifier.citationНікітченко Микола Степанович. Першопорядкові логіки із квазіарними та n-арними предикатами / Нікітченко М. С., Шкільняк С. С. // Наукові записки НаУКМА : Комп'ютерні науки. - 2016. - Т. 190. - С. 16-22.uk
dc.identifier.urihttps://ekmair.ukma.edu.ua/handle/123456789/11116
dc.language.isoukuk
dc.relation.sourceНаукові записки НаУКМА: Комп'ютерні наукиuk
dc.statuspublished earlieruk
dc.subjectлогікаuk
dc.subjectквазіарний предикатuk
dc.subjectn-арний предикатuk
dc.subjectлогічний наслідокuk
dc.subjectlogicuk
dc.subjectquasiary predicateen
dc.subjectn-ary predicateen
dc.subjectlogical consequenceen
dc.titleПершопорядкові логіки із квазіарними та n-арними предикатамиen
dc.title.alternativeFirst-Order Logics with Quasi-Ary and N-Ary Predicatesuk
dc.typeArticleuk
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Nikitchenko_Shkilniak_Pershoporiadkovi_lohiky.pdf
Size:
912.25 KB
Format:
Adobe Portable Document Format
Description:
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
7.54 KB
Format:
Item-specific license agreed upon to submission
Description: