Propositional logics of partial predicates with composition of predicate complement
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 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
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.
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.