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

Computer Science Journal of Moldova

Stepan Shkilniak¹  Oksana Shkilniak¹  Tohrul Mamedov¹  Mykola Nikitchenko² 

[1] ;Taras Shevchenko National University of Kyiv, Ukraine;

关键词: partial predicate;    quasiary predicate;    program logic;    predicate logic;    soundness and completeness;   

DOI  :  

来源: DOAJ

【 摘 要 】

Partial quasiary predicates are used in programming for representing program semantics and in logic for formalizing predicates 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 construct 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 (composition). In the paper we define one of such logics called first-order logic of partial quasiary predicates with the complement composition. For this logic a special consequence relation called irrefutability consequence relation under undefinedness conditions is introduced. We study its properties, construct a sequent calculus for it and prove soundness and completeness of this calculus.

【 授权许可】

Unknown