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 条
  • [31] Intuitionistic propositional probability logic
    Ilic-Stepic, Anelina
    Knezevic, Mateja
    Ognjanovic, Zoran
    MATHEMATICAL LOGIC QUARTERLY, 2022, 68 (04) : 479 - 495
  • [32] Bisimulation and propositional intuitionistic logic
    Patterson, A
    CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 347 - 360
  • [33] A Tutorial on Stålmarck's Proof Procedure for Propositional Logic
    Mary Sheeran
    Gunnar Stålmarck
    Formal Methods in System Design, 2000, 16 : 23 - 58
  • [34] A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic
    Fiorentini, Camillo
    Gore, Rajeev
    Graham-Lengrand, Stephane
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2019, 2019, 11714 : 111 - 129
  • [35] Quantifiers in logic and proof-search using permissive-nominal terms and sets
    Gabbay, Murdoch J.
    Wirth, Claus-Peter
    JOURNAL OF LOGIC AND COMPUTATION, 2015, 25 (02) : 473 - 523
  • [36] Detecting loops during proof search in propositional affine logic
    Lutovac, T
    Harland, J
    JOURNAL OF LOGIC AND COMPUTATION, 2006, 16 (01) : 61 - 133
  • [37] ON RECONSTRUCTABILITY OF CLASSICAL PROPOSITIONAL LOGIC IN INTUITIONISTIC LOGIC
    WOJCICKI, R
    BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1970, 18 (08): : 421 - &
  • [38] THE PROOF-INTUITIONISTIC PROPOSITIONAL CALCULUS
    KUZNETSOV, AV
    DOKLADY AKADEMII NAUK SSSR, 1985, 283 (01): : 27 - 30
  • [39] Interactive proof-search for equational reasoning
    Miranda-Perea, Favio E.
    Gonzalez Huesca, Lourdes del Carmen
    Selene Linares-Arevalo, P.
    LOGIC JOURNAL OF THE IGPL, 2020, 28 (06) : 1155 - 1181
  • [40] On Different Proof-Search Strategies for Orthologic
    Uwe Egly
    Hans Tompits
    Studia Logica, 2003, 73 (1) : 131 - 152
12345