Open AccessNatural deduction in a paracomplete setting
Author(s) -
Alexander Bolotov,
Vasilyi Shangin
Publication year - 2014
Publication title -
logičeskie issledovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2413-2713
pISSN - 2074-1472
DOI - 10.21146/2074-1472-2014-20-0-222-245
Subject(s) - natural deduction , mathematical proof , natural (archaeology) , sequent calculus , computer science , calculus (dental) , mathematics , proof theory , automated theorem proving , algorithm , programming language , medicine , geometry , archaeology , dentistry , history
In this paper we present the automated proof search technique in natural deduction paracomplete logic. Here, 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 of the type p _ ¬p, are not valid. In this paper 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.