{"id":"arxiv:2410.23765","kind":"preprint","title":"Intuitionistic Propositional Logic in Lean","authors":["Dafina Trufaş"],"author_count":1,"year":2024,"published":"2024-10-31","venue":"EPTCS 410, 2024, pp. 133-149","cited_by":null,"doi":"10.4204/eptcs.410.9","arxiv_id":"2410.23765","nct_id":null,"source_url":"https://arxiv.org/abs/2410.23765","archive_url":"https://space-kitty.com/papers/arxiv:2410.23765","updated":"2024-10-31","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2410.23765","abstract":"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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}