Paracomplete logic Kl: natural deduction, its automation, complexity and applications

In the development of many modern software solutions where the underlying systems are complex, dynamic and heterogeneous, the significance of specification-based verification is well accepted. However, often parts of the specification may not be known. Yet reasoning based on such incomplete specifications is very desirable. Here, paracomplete logics seem to be an appropriate formal setup: opposite to Tarski’s theory of truth with its principle of bivalence, in these logics a statement and its negation may be both untrue. An immediate result is that the law of excluded middle becomes invalid. In this paper we show a way to apply an automatic proof searching procedure for the paracomplete logic Kl to reason about incomplete information systems. We provide an original account of complexity of natural deduction systems, leading us closer to the efficiency of the presented proof search algorithm. Moreover, we have turned the assumptions management into an advantage showing the applicability of the proposed technique to assume-guarantee reasoning