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 条

[1] A bounded translation of intuitionistic propositional logic into basic propositional logic
Aghaei, M
Ardeshir, M
MATHEMATICAL LOGIC QUARTERLY, 2000, 46 (02) : 199 - 206
[2] CLASSICAL PROPOSITIONAL LOGIC AND DECIDABILITY OF VARIABLES IN INTUITIONISTIC PROPOSITIONAL LOGIC
Ishihara, Hajime
LOGICAL METHODS IN COMPUTER SCIENCE, 2014, 10 (03) : 1 - 7
[3] A CHARACTERIZATION OF INTUITIONISTIC PROPOSITIONAL LOGIC
MUTI, N
NAGOYA MATHEMATICAL JOURNAL, 1970, 37 : 131 - &
[4] Intuitionistic propositional probability logic
Ilic-Stepic, Anelina
Knezevic, Mateja
Ognjanovic, Zoran
MATHEMATICAL LOGIC QUARTERLY, 2022, 68 (04) : 479 - 495
[5] Bisimulation and propositional intuitionistic logic
Patterson, A
CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 347 - 360
[6] 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 - &
[7] Interpreting intuitionistic propositional logic in terms of intuitionistic protothetics
Yashin A.D.
Algebra and Logic, 2002, 41 (1) : 59 - 64
[8] Intuitionistic Propositional Logic with Galois Negations
Ma, Minghui
Li, Guiying
STUDIA LOGICA, 2023, 111 (01) : 21 - 56
[9] Intuitionistic propositional logic with Galois connections
Dzik, Wojciech
Jarvinen, Jouni
Kondo, Michiro
LOGIC JOURNAL OF THE IGPL, 2010, 18 (06) : 837 - 858
[10] Computations in fragments of intuitionistic propositional logic
1600, Publ by Kluwer Academic Publishers Group, Dordrecht, Neth (07):

← 1 2 3 4 5 →