Machine-Checked Meta-theory of Dual-Tableaux for Intuitionistic Logic
We describe how we formalised the meta-theory of Melvin Fitting’s dual-tableaux calculi for intuitionistic logic using the HOL4 interactive theorem prover. The paper is intended for readers familiar with dual-tableaux who might be interested in, but daunted by, the idea of formalising the required notions in a modern interactive theorem prover.
We are grateful to the anonymous reviewers for their suggestions for improvements.
- Dawson, J. E. & Goré, R. (2002). Formalised cut admissibility for display logic. In V. A. Carreno, C. A. Munoz, & S. Tahar (Eds.), TPHOLs02: Proceedings of the 15th international conference on theorem proving in higher order logics (Vol. 2410, pp. 131–147). Lecture Notes in Computer Science. Berlin: Springer.Google Scholar
- Fitting, M. (2018). Tableaus and dual tableaus. In J. Golińska-Pilarek & M. Zawidzki (Eds.), Ewa Orłowska on Relational Methods in Logic and Computer Science (pp. 105–128). Outstanding Contributions to Logic. Berlin: Springer.Google Scholar
- Gordon, M. (2008). Twenty years of theorem proving for HOLs past, present and future. In O. A. Mohamed, C. A. Muñoz, & S. Tahar (Eds.), Proceedings of Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008 (Vol. 5170, pp. 1–5). Lecture Notes in Computer Science. Montreal: Springer.Google Scholar