Institutul de Matematică şi Informatică "Vladimir Andrunachievici"
Universitatea de Stat din MoldovaRO EN
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.
– 0.18 Mb
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:
E-mail:
Fulltext
– 0.18 Mb
Contents
- Quantitative Expressiveness of Instruction Sequence Classes for Computation on Single Bit Registers
- Completeness of the First-Order Logic of Partial Quasiary Predicates with the Complement Composition
- New Bounds For Degree Sequence Of Graphs
- On the signed Italian domination of graphs
- A Novel Hybrid Algorithm for Minimizing Total Weighted Tardiness Cost
- Mixed Algorithm for Combinations Generation
- In memoriam of Yurii Rogozhin
