Propositional logics of partial predicates with composition of predicate complement
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 operation...
Saved in:
| Date: | 2019 |
|---|---|
| Main Authors: | , , , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
PROBLEMS IN PROGRAMMING
2019
|
| Subjects: | |
| Online Access: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/344 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Problems in programming |
| Download file: |  |
Institution
Problems in programming| Summary: | 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 propositional 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 consider 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 predicates, 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 formulas 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 |
|---|