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 条

[31] The Lambek Calculus Extended with Intuitionistic Propositional Logic
Kaminski, Michael
Francez, Nissim
STUDIA LOGICA, 2016, 104 (05) : 1051 - 1082
[32] FUNCTIONAL COMPLETENESS FOR SUBSYSTEMS OF INTUITIONISTIC PROPOSITIONAL LOGIC
WANSING, H
JOURNAL OF PHILOSOPHICAL LOGIC, 1993, 22 (03) : 303 - 321
[33] A Forward Unprovability Calculus for Intuitionistic Propositional Logic
Fiorentini, Camillo
Ferrari, Mauro
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2017, 2017, 10501 : 114 - 130
[34] A note on decidability of variables in intuitionistic propositional logic
Ishii, Katsumasa
MATHEMATICAL LOGIC QUARTERLY, 2018, 64 (03) : 183 - 184
[35] Propositional quantification in the monadic fragment of intuitionistic logic
Polacik, T
JOURNAL OF SYMBOLIC LOGIC, 1998, 63 (01) : 269 - 300
[36] Justification logic and type theory as formalizations of intuitionistic propositional logic
DeBoer, Neil J.
JOURNAL OF LOGIC AND COMPUTATION, 2022, 32 (08) : 1531 - 1557
[37] Doing logic by computer: interpolation in fragments of intuitionistic propositional logic
Hendriks, L
ANNALS OF PURE AND APPLIED LOGIC, 2000, 104 (1-3) : 97 - 112
[38] Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
Villadsen, Jorgen
From, Asta Halkjaer
Blackburn, Patrick
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (354): : 71 - 85
[39] Irreflexive Modality in the Intuitionistic Propositional Logic and Novikov Completeness
A. D. Yashin
Journal of Philosophical Logic, 1999, 28 : 175 - 197
[40] (α, β)-Ordered Linear Resolution of Intuitionistic Fuzzy Propositional Logic
Li, Baihua
Li, Xiaonan
Pan, Chang
Zou, Li
Xu, Yang
2015 10TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (ISKE), 2015, : 341 - 344

← 1 2 3 4 5 →