Paracomplete Logic Kl — Natural Deduction, its Automation, Complexity and Applicationsстатья

Информация о цитировании статьи получена из Web of Science
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 апреля 2019 г.

Работа с статьей


[1] Bolotov A., Kozhemiachenko D., Shangin V. Paracomplete logic kl — natural deduction, its automation, complexity and applications // Journal of Applied Logics - IfCoLoG Journal of Logics and their Applications. — 2018. — Vol. 5, no. 1. — P. 221–263. 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 how to apply an automatic proof searching procedure for the natural deduction formulation of the paracomplete logic Kl to reason about incomplete information systems. We provide an original account of complexity of natural deduction systems, which leads us closer to the efficiency of the presented proof search algorithm. Moreover, we have turned the assumptions management into an advantage by showing the applicability of the proposed technique to assume-guarantee reasoning.

Публикация в формате сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл скрыть