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

Type | Journal article |
---|

Authors | Bolotov, A., Kozhemiachenko, D. and Shangin, V. |
---|

Abstract | 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. |
---|

Keywords | natural deduction, automated reasoning, proof search, incomplete specification, assume-guarantee reasoning, component based modelling |
---|

Journal | Journal of Applied Logics - IfCoLog Journal of Logics and their Applications |
---|

Journal citation | 5 (1), pp. 221-261 |
---|

ISSN | 2055-3706 |
---|

Year | 2018 |
---|

Publisher | College Publications |
---|

Publisher's version | File Access Level Open (open metadata and files) |
---|

Web address (URL) | http://www.collegepublications.co.uk/journals/ifcolog/?00021 |
---|

Publication dates |
---|

*Published* | 28 Feb 2018 |
---|

License | CC BY-NC-ND 4.0 |
---|