Abstract
We formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. Our formalization precisely details the structure of this proof method.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the ESSLLI & WeSSLLI Student Session 2020 |
| Publication date | 2020 |
| Pages | 1-12 |
| Publication status | Published - 2020 |
| Event | Web Summer School in Logic, Language, and Information - Virtual event Duration: 11 Jul 2020 → 17 Jul 2020 https://www.brandeis.edu/nasslli2020/index.html |
Workshop
| Workshop | Web Summer School in Logic, Language, and Information |
|---|---|
| Location | Virtual event |
| Period | 11/07/2020 → 17/07/2020 |
| Internet address |
Keywords
- Propositional logic
- Henkin-style completeness
- Isabelle/HOL