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 条

[41] Interpreting intuitionistic propositional logic in terms of intuitionistic protothetics
Yashin A.D.
Algebra and Logic, 2002, 41 (1) : 59 - 64
[42] Intuitionistic Propositional Logic with Galois Negations
Ma, Minghui
Li, Guiying
STUDIA LOGICA, 2023, 111 (01) : 21 - 56
[43] Intuitionistic propositional logic with Galois connections
Dzik, Wojciech
Jarvinen, Jouni
Kondo, Michiro
LOGIC JOURNAL OF THE IGPL, 2010, 18 (06) : 837 - 858
[44] Computations in fragments of intuitionistic propositional logic
1600, Publ by Kluwer Academic Publishers Group, Dordrecht, Neth (07):
[45] On sequent calculi for intuitionistic propositional logic
Svejdar, Vitezslav
COMMENTATIONES MATHEMATICAE UNIVERSITATIS CAROLINAE, 2006, 47 (01): : 159 - 173
[46] Intuitionistic Propositional Logic with Galois Negations
Minghui Ma
Guiying Li
Studia Logica, 2023, 111 : 21 - 56
[47] THE DECIDABILITY OF DEPENDENCY IN INTUITIONISTIC PROPOSITIONAL LOGIC
DEJONGH, D
CHAGROVA, LA
JOURNAL OF SYMBOLIC LOGIC, 1995, 60 (02) : 498 - 504
[48] A Lindstrom Theorem for Intuitionistic Propositional Logic
Badia, Guillermo
Olkhovikov, Grigory
NOTRE DAME JOURNAL OF FORMAL LOGIC, 2020, 61 (01) : 11 - 30
[49] A Proof-Theoretic Analysis of the Meaning of a Formula in a Combination of Intuitionistic and Classical Propositional Logic
Toyooka, Masanobu
LOGIC AND ENGINEERING OF NATURAL LANGUAGE SEMANTICS, LENLS19, 2023, 14213 : 100 - 119
[50] On the complexity of propositional quantification in intuitionistic logic
Kremer, P
JOURNAL OF SYMBOLIC LOGIC, 1997, 62 (02) : 529 - 544

← 1 2 3 4 5 →