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
相关论文
共 14 条
  • [1] [Anonymous], 2000, SHORT INTRO INTUITIO
  • [2] THE CALCULUS OF CONSTRUCTIONS
    COQUAND, T
    HUET, G
    [J]. INFORMATION AND COMPUTATION, 1988, 76 (2-3) : 95 - 120
  • [3] The Lean Theorem Prover (System Description)
    de Moura, Leonardo
    Kong, Soonho
    Avigad, Jeremy
    van Doorn, Floris
    von Raumer, Jakob
    [J]. AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 378 - 388
  • [4] Fitting M. C., 1968, Studies in Logic and the Foundationsof Mathematics, DOI [10.2307/2271564, DOI 10.2307/2271564]
  • [5] Georgescu G., 1995, Lecture Notes
  • [6] Georgescu G., 1995, Lecture Notes
  • [7] Godel K., 1958, Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes, P280, DOI [10.1111/j.1746-8361.1958.tb01464.x, DOI 10.1111/J.1746-8361.1958.TB01464.X]
  • [8] Kuznetsov S., 2017, Propositional Intuitionistic Logic
  • [9] leanprover-community.github, A Mathlib Overview
  • [10] Liao B., 2023, Logics for Al and Law, P36
12