First-order composition-nominative logics with predicates of weak equality and of strong equality
Abstract
Development of the new software-oriented logical formalisms is a topical problem. The paper introduces logics of partial predicates with predicate complement and equality predicates, we denote them LCE. They extend logics of quasiary predicates with equality and logics with predicate complement. The composition of the predicate complement is used in Floyd-Hoare program logics’ extensions on the class of partial predicates. We define predicates of weak equality and of strong equality. Thus, LCE with predicates of weak equality (denoted by LCEw) and LCE with predicates of strong equality (denoted by LCEs) can be specified. LCE can be studied on the first order and renominative levels. We consider composition algebras of LCE, investigate properties of their compositions and describe first order languages of such logics. We concentrate on the properties related to the equality predicates and the composition of the predicate complement. Various variants of logical consequence relations for the first order LCE are introduced and studied: P|=T, P|=F, R|=T, R|=F, P|=TF, R|=TF, P|=IR. In particular, we obtained that LCEw are somewhat degenerate, as for them all the relations are incorrect except for the irrefutability logical consequence relation under the conditions of undefinedness |=IR^. At the same time, all of the listed relations are correct for LCEs. Properties of the logical consequence relations are the semantic basis for construction of the respective calculi of sequential type. Further investigation of logical consequence relations for LCE includes adding the conditions of undefinedness and constructing the corresponding sequent calculi; it is planned to be displayed in the forthcoming articles.
Problems in programming 2019; 3: 28-44
Keywords
Full Text:
PDF (Українська)References
ABRAMSKY, S., GABBAY, D. and MAIBAUM, T. (editors). (1993-2000). Handbook of Logic in Computer Science Oxford University Press, Vol. 1-5.
HOARE, C. (1969). An axiomatic basis for computer programming, Comm. ACM 12(10), 576-580, 1969. CrossRef
APT, K. (1981). Ten years of Hoare's logic: a survey - part I, ACM Trans. Program. Lang. Syst. 3(4), pp. 431-483. CrossRef
IVANOV, I. and NIKITCHENKO, M. (2018). On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions. In Proceedings of the 14th International Conference on ICT. Vol 2104 of CEUR Workshop Proc., pp. 716-724.
IVANOV, I. and NIKITCHENKO, M. (2019). Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement. In Communication. in Computer and Information Science. Vol. 1007. Springer, Cham, pp. 71-88. CrossRef
NIKITCHENKO, M., SHKILNIAK, O., SHKILNIAK, S. and MAMEDOV, T. (2019). Propositional logics of partial predicates with composition of predicate complement. In Problems in Progamming. No 1. P. 3-13 (in ukr). CrossRef
NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2019). Pure first-order logics of quasiary predicates with the composition of predicate complement. In Proceedings of the XIXh International Conference "Dynamical systems modelling and stability investigation", pp. 371-373 (in ukr). CrossRef
SHKILNIAK, O. (2019). Relations of logical consequence in logics of partial predicates with composition of predicate complement. In Problems in Progamming. No 3 (in ukr). CrossRef
NIKITCHENKO, M. and SHKILNIAK, S. (2017). Pure first-order quasiary logics with equality predicates. In Problems in Progamming. No 2. P. 3-23 (in ukr).
NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2016). Pure first-order logics of quasiary predicates. In Problems in Progamming. No 2-3. P. 73-86 (in ukr).
DOI: https://doi.org/10.15407/pp2019.03.028
Refbacks
- There are currently no refbacks.