First-order composition-nominative logics with predicates of weak equality and of strong equality

S.S. Shkilniak

Abstract


Development of the new software-oriented logical formalisms is a topical problem. The paper introduces lo­gics of partial predicates with predicate complement and equality predicates, we denote them LCE. They ex­tend logics of quasiary predicates with equality and logics with predicate complement. The composition of the predicate complement is used in Floyd-Hoare pro­­gram logics’ extensions on the class of partial predi­cates. 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 con­struction of the respective calculi of sequential type. Further investigation of logical consequence relations for LCE includes adding the conditions of undefined­ness and constructing the corresponding sequent calcu­li; it is planned to be displayed in the forthcoming ar­ticles.

 Problems in programming 2019; 3: 28-44

  

Keywords


logic; predicate; composition; equality; logical consequence

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.