Tackling Incomplete System Specifications Using Natural Deduction in the Paracomplete Setting

In many modern computer applications the significance of specification based verification is well accepted. However, when we deal with such complex processes as the integration of heterogeneous systems, parts of specification may be not known. Therefore it is important to have techniques that are able to cope with such incomplete information. An adequate formal setup is given by so called Para complete logics, where, contrary to the classical framework, for some statements we do not have evidence to conclude if they are true or false. As a consequence, for example, the law of excluded middle is not valid. In this paper we justify how the automated proof search technique for Para complete logic PComp can be efficiently applied to the reasoning about systems with incomplete information. Note that for many researchers, one of the core features of natural deduction, the opportunity to introduce arbitrary formulae as assumptions, has been a point of great scepticism regarding thievery possibility of the automation of the proof search. Here, not only we show the contrary, but we also turned the assumptions management into an advantage showing the applicability of the proposed technique to assume-guarantee reasoning.