Logo BSU

Please use this identifier to cite or link to this item: http://elib.bsu.by/handle/123456789/162882
Title: The Inverse Method Application for Non-Classical Logics
Authors: Pavlov, V.
Paky, V.
Issue Date: 2015
Publisher: Minsk : Education and Upbringing
Citation: Nonlinear Phenomena in Complex Systems. - 2015. - Vol. 18, N 2. - P. 181-190
Abstract: Maslov’s inverse method is an automated theorem proving method: it can be used to develop computer programs that prove theorems automatically (such programs are called theorem provers). The inverse method can be applied to a wide range of logical calculi: propositional logic, first-order logic, intuitionistic logic, modal logics etc. We give a brief historical background of the inverse method, then discuss existing modifications and implementations of the inverse method for non-classical logics (intuitionistic logic, modal logics and some other logics). We introduce a variant of the inverse method for intuitionistic logic - a logic that allows only constructive proofs, i.e. proofs that construct an existing mathematical object instead of just establishing the fact that such an object exists. In short, intuitionistic logic can be seen as classical logic without the law of excluded middle A ∨ ¬A or the law of double negation elimination ¬¬A ⊃ A. So, classical proofs by contradiction are not allowed in intuitionistic logic. We discuss our experimental program implementation of the inverse method for intuitionistic logic: some details of implementation, results of experiments on ILTP problems (ILTP is a common library of test problems for intuitionistic theorem provers).
URI: http://elib.bsu.by/handle/123456789/162882
ISSN: 1561 - 4085
Appears in Collections:2015. Volume 18. Number 2

Files in This Item:
File Description SizeFormat 
v18no2p181.pdf137,74 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.