A proof-search procedure for intuitionistic propositional logic

被引：0
|
作者：
Alonderis, R. [1 ]
机构：
[1] Vilnius State Univ, Inst Math & Informat, LT-2600 Vilnius, Lithuania
来源：
ARCHIVE FOR MATHEMATICAL LOGIC | 2013年 / 52卷 / 7-8期
关键词：
Propositional intuitionistic logic; Sequent calculus; Glivenko's Theorem;
D O I：
10.1007/s00153-013-0342-y
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko's Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.
引用
收藏
页码：759 / 778
页数：20
相关论文
共 50 条
12345