RO  EN
IMCS/Publications/CSJM/Issues/CSJM v.27, n.2 (80), 2019/

Completeness of the First-Order Logic of Partial Quasiary Predicates with the Complement Composition

Authors: Mykola Nikitchenko, Oksana Shkilniak, Stepan Shkilniak, Tohrul Mamedov
Keywords: partial predicate, quasiary predicate, program logic, predicate logic, soundness and completeness.

Abstract

Partial quasiary predicates are used in programming for rep- resenting program semantics and in logic for formalizing predi- cates over partial variable assignments. Such predicates do not have fixed arity therefore they may be treated as mappings over partial data. Obtained logics are not expressive enough to con- struct sound axiomatic systems of Floyd–Hoare type. To increase expressibility of such logics, oriented on quasiary predicates, we extend their language with the complement operation (composi- tion). In the paper we define one of such logics called first-order logic of partial quasiary predicates with the complement com- position. For this logic a special consequence relation called ir- refutability consequence relation under undefinedness conditions is introduced. We study its properties, construct a sequent calcu- lus for it and prove soundness and completeness of this calculus.

Taras Shevchenko National University of Kyiv, Ukraine
E-mail:



Fulltext

Adobe PDF document – 0.18 Mb