Open AccessAbout proof-search in intuitionistic natural deduction calculus using partial Skolemization
Author(s) -
Oleg Okhotnikov
Publication year - 2020
Publication title -
journal of physics. conference series
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.21
H-Index - 85
eISSN - 1742-6596
pISSN - 1742-6588
DOI - 10.1088/1742-6596/1680/1/012038
Subject(s) - natural deduction , soundness , calculus (dental) , mathematics , completeness (order theory) , sequent calculus , structural proof theory , cut elimination theorem , curry–howard correspondence , proof calculus , algorithm , proof theory , discrete mathematics , computer science , mathematical proof , programming language , mathematical analysis , medicine , geometry , dentistry
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.