Please use this identifier to cite or link to this item: http://hdl.handle.net/10995/102373
Title: About proof-search in intuitionistic natural deduction calculus using partial Skolemization
Authors: Okhotnikov, O.
Issue Date: 2020
Publisher: IOP Publishing Ltd
Citation: Okhotnikov O. About proof-search in intuitionistic natural deduction calculus using partial Skolemization / O. Okhotnikov. — DOI 10.1088/1742-6596/1680/1/012038 // Journal of Physics: Conference Series. — 2020. — Vol. 1680. — Iss. 1. — 012038.
Abstract: In this paper, automated proof search in single-conclusion sequential variant of intuitionistic and minimal predicate calculus is considered. In this algorithm, meta-variables and partial Skolemization are used. Theorems of soundness and completeness for the considered algorithm are proved. © Published under licence by IOP Publishing Ltd.
Keywords: PHYSICS
AUTOMATED PROOFS
NATURAL DEDUCTION
PROOF SEARCH
SEQUENTIAL VARIANTS
SKOLEMIZATION
SOUNDNESS AND COMPLETENESS
CALCULATIONS
URI: http://hdl.handle.net/10995/102373
Access: info:eu-repo/semantics/openAccess
SCOPUS ID: 85098580327
PURE ID: 20375542
1a822a2e-be8d-419b-85ab-150eb8f3f886
ISSN: 17426588
DOI: 10.1088/1742-6596/1680/1/012038
Appears in Collections:Научные публикации, проиндексированные в SCOPUS и WoS CC

Files in This Item:
File Description SizeFormat 
2-s2.0-85098580327.pdf583,65 kBAdobe PDFView/Open


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