Intuitionistic Propositional Logic in Lean

被引：0

作者：

Trufas, Dafina ^{[1
]}

机构：

[1] Univ Bucharest, Fac Math & Comp Sci, LOS, Inst Log & Data Sci, Bucharest, Romania

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2024年 / 410期

关键词：

D O I：

10.4204/EPTCS.410.8

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.

引用

页数：172

共 50 条

[41] Decision procedures for intuitionistic propositional logic by program extraction
Weich, K
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 292 - 306
[42] Epistemic extensions of combined classical and intuitionistic propositional logic
Lewitzka, Steffen
LOGIC JOURNAL OF THE IGPL, 2017, 25 (03) : 309 - 324
[43] (α, β)-Ordered linear resolution of intuitionistic fuzzy propositional logic
Zou, Li
Li, XiaoNan
Pan, Chang
Liu, Xin
INFORMATION SCIENCES, 2017, 414 : 329 - 339
[44] Irreflexive modality in the intuitionistic propositional logic and Novikov completeness
Yashin, AD
JOURNAL OF PHILOSOPHICAL LOGIC, 1999, 28 (02) : 175 - 197
[45] A proof-search procedure for intuitionistic propositional logic
R. Alonderis
Archive for Mathematical Logic, 2013, 52 : 759 - 778
[46] Intuitionistic propositional logic with only equivalence has no interpolation
Hendriks, L
JOURNAL OF LOGIC AND COMPUTATION, 1998, 8 (04) : 589 - 593
[47] A secondary semantics for second order intuitionistic propositional logic
Ferrari, M
Fiorentini, C
Fiorino, G
MATHEMATICAL LOGIC QUARTERLY, 2004, 50 (02) : 202 - 210
[48] A NOTE ON GENTZENS DECISION PROCEDURE FOR INTUITIONISTIC PROPOSITIONAL LOGIC
DOSEN, K
ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1987, 33 (05): : 453 - 456
[49] Timing analysis of combinational circuits in intuitionistic propositional logic
Mendler, M
FORMAL METHODS IN SYSTEM DESIGN, 2000, 17 (01) : 5 - 37
[50] On the polynomial-space completeness of intuitionistic propositional logic
Vítězslav Švejdar
Archive for Mathematical Logic, 2003, 42 : 711 - 716

← 1 2 3 4 5 →