Propositional logics of partial predicates with composition of predicate complement

M.S. Nikitchenko, O.S. Shkilniak, S.S. Shkilniak, T.A. Mamedov

Abstract


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


Keywords


logic; partial predicate; logical consequence; sequent сalculus

References


Abramsky S., Gabbay D. and Maibaum T. (editors). (1993–2000). Handbook of Logic in Computer Science Oxford University Press, Vol. 1–5.

Avron A. and Zamansky A. (2011). Non-deterministic semantics for logical systems. In Handbook of Philosophical Logic, D.M. Gabbay, F. Guenthner (eds.), 2nd ed., Vol. 16, Springer Netherlands. P. 227–304. CrossRef

Gries D. and Schneider F. (1995). Avoiding the undefined by underspecification. Springer Berlin Heidelberg. CrossRef

Hähnle R. (2005). Many-valued logic, partiality, and abstraction in formal specification languages. In Logic Journal of the IGPL, 13. P. 415–433. CrossRef

Jones C. (2006). Reasoning about partial functions in the formal development of programs. In Proceedings of AVoCS'05. Vol. 145. Elsevier, Electronic Notes in Theoretical Computer Science. P. 3–25. CrossRef

Nikitchenko M. and Shkilniak S. (2015). Semantic Properties of Logics of Quasiary Predicates. In Workshop on Foundations of Informatics: Proceedings FOI-2015. Chisinau, Moldova. P. 180–197.

Nikitchenko M., Shkilniak O. and Shkilniak S. (2016). Pure first-order logics of quasiary predicates. In Problems in Progamming. N 2–3. P. 73–86 (in ukr).

Nikitchenko M. and Shkilniak S. (2017). Algebras and logics of partial quasiary predicates. In Algebra and Discrete Mathematics. Vol. 23. N 2. P. 263–278.

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. P. 716–724.

Kleene S. (1973) Mathematical Logic. Moscow: Mir (in rus).

Kleene S. (1952) Introductions to Metamathematics. Van Nostrand, Princeton.

Nikitchenko M., Shkilniak O. and Shkilniak S. (2018). Logics of general non-deterministic predicates: semantic aspects. In Problems in Progamming. N 2–3. P. 31–45 (in ukr). CrossRef




DOI: https://doi.org/10.15407/pp2019.01.003

Refbacks

  • There are currently no refbacks.