Abstract
We present a concise formalization in the proof assistant Isabelle/HOL of a sequent calculus and a naive automatic theorem prover implementing a sound and complete proof search strategy for classical implicational logic.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of Isabelle Workshop 2024 |
| Number of pages | 15 |
| Publication date | 2024 |
| Publication status | Published - 2024 |
| Event | Isabelle Workshop 2024 - Hybrid event, Tbilisi , Georgia Duration: 14 Sept 2024 → 14 Sept 2024 |
Workshop
| Workshop | Isabelle Workshop 2024 |
|---|---|
| Location | Hybrid event |
| Country/Territory | Georgia |
| City | Tbilisi |
| Period | 14/09/2024 → 14/09/2024 |