ИСТИНА

In the framework of specification based verification often part of specification is not known. In this paper we present the automated proof search technique to assist reasoning about such specifications with incomplete information. An adequate formal set up is given by so called paracomplete logics, where for some statements we do not have evidence to conclude if they are true or false, as it happens in the classical framework. As a consequence, for example, formulae expressing the law of excluded middle is not in general valid. We formulate the natural deduction system for paracomplete logic PComp, explain its main concepts, define proof searching techniques and the searching algorithm providing examples proofs. The logic PComp is useful to reason about uncertain systems where the law of excluded middle does not hold.