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 条

[1] A proof-search procedure for intuitionistic propositional logic
R. Alonderis
Archive for Mathematical Logic, 2013, 52 : 759 - 778
[2] Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic
Mauro Ferrari
Camillo Fiorentini
Journal of Automated Reasoning, 2019, 62 : 127 - 167
[3] Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic
Ferrari, Mauro
Fiorentini, Camillo
JOURNAL OF AUTOMATED REASONING, 2019, 62 (01) : 127 - 167
[4] Proof-search in intuitionistic logic based on constraint satisfaction
Voronkov, A
THEOREM PROVING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1996, 1071 : 312 - 329
[5] Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
Ferrari, Mauro
Fiorentini, Camillo
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015), 2015, 9323 : 237 - 252
[6] Proof-search, analytic tableaux, models and counter-models, in Hypo constructive semantics for Minimal and Intuitionistic Propositional Logic
Sanz, Wagner
Journal of Applied Logics, 2022, 9 (01): : 541 - 572
[7] PROOF-SEARCH, ANALYTIC TABLEAUX, MODELS AND COUNTER-MODELS, IN HYPO CONSTRUCTIVE SEMANTICS FOR MINIMAL AND INTUITIONISTIC PROPOSITIONAL LOGIC
Sanz, Wagner
JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS, 2022, 9 (01): : 541 - 571
[8] Efficient SAT-based Proof Search in Intuitionistic Propositional Logic
Fiorentini, Camillo
AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 217 - 233
[9] A proof-search system for the logic of likelihood
Alonderis, R.
Giedra, H.
LOGIC JOURNAL OF THE IGPL, 2020, 28 (03) : 261 - 280
[10] Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
Voronkov, A., 1600, Kluwer Academic Publishers (30):

← 1 2 3 4 5 →