Propositional logics of partial predicates with composition of predicate complement

• Дата: 2019
• Автори: Nikitchenko, M.S., Shkilniak, O.S., Shkilniak, S.S., Mamedov, T.A.
• Формат: Стаття
• Мова: Ukrainian
• Опубліковано: Інститут програмних систем НАН України 2019
• Теми: logic; partial predicate; logical consequence; sequent сalculus; UDC 004.42:510.69
• Онлайн доступ: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/344
• Назва журналу: Problems in programming

The paper studies new software-oriented logical formalisms – the logics of partial predicates with predicate complement. Such logics are denoted LC. A characteristic feature of these logics is the presence of a special non-monotonic operation (composition) of the predicate complement. Such operations are used in various versions of the Floyd-Hoare logic with partial pre- and post-conditions. Properties of LC proposi­tional compositions are similar to the properties of the traditional logical connectives. Properties of the new composition of the predicate complement are investigated. The class of P-predicates (partial single-valued) is closed under the composition of the predicate complement, but the class of T-predicates (total) is not closed. Therefore, it is possible to con­sider the general class LC – the logic of R-predicates (relational predicates) with the composition of the predicate complement, and its subclass LPC – the logic of P-predicates with such a composition. The focus of the work is the study of PLC – propositional LC. Propositional composition algebras and PLC languages are described. For LC of partial single-valued predi­cates, an irrefutability logical consequence relation |=IR^ is proposed and investigated under the conditions of undefinedness. The conditions for the validity of the |=IR^ and the properties of the decomposition of for­mulas are given. Based on the properties of the |=IR^, for PLC of P-predicates a calculus of sequential type is constructed. The basic sequential forms of this calculus and closure conditions of the sequents are given. For the constructed calculus, correctness and completeness theorems are hold. Proofs of these theorems will be given in the forthcoming articles.Problems in programming 2019; 1: 03-13