Intuitionistic Propositional Logic in Lean
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915000557240320 |
|---|---|
| author | Trufaş, Dafina |
| author_facet | Trufaş, Dafina |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_23765 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Intuitionistic Propositional Logic in Lean Trufaş, Dafina Logic in Computer Science 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. |
| title | Intuitionistic Propositional Logic in Lean |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.23765 |