Paracomplete Logic Kl — Natural Deduction, its Automation, Complexity and Applicationsстатья
Информация о цитировании статьи получена из
Web of Science
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 апреля 2019 г.
Аннотация:In the development of many modern software solutions where the underlyingsystems are complex, dynamic and heterogeneous, the significance ofspecification-based verification is well accepted. However, often parts of thespecification may not be known. Yet reasoning based on such incomplete specificationsis very desirable. Here, paracomplete logics seem to be an appropriateformal 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. Animmediate result is that the law of excluded middle becomes invalid. In thispaper we show how to apply an automatic proof searching procedure for thenatural deduction formulation of the paracomplete logic Kl to reason aboutincomplete information systems. We provide an original account of complexityof natural deduction systems, which leads us closer to the efficiency of thepresented proof search algorithm. Moreover, we have turned the assumptionsmanagement into an advantage by showing the applicability of the proposedtechnique to assume-guarantee reasoning.