Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The predicates tab_val_aux R pv x sfss and sfs_val_aux R pv y sf may be false only at worlds \(x = \texttt {u}\) and \(y = \texttt {v}\) respectively, where u and v are different future worlds of w, which make tab_val_aux R pv w sfss and sfs_val_aux R pv w {sf} equal (both false); however adding context may change the valuation to make it true at world u but not v, or vice versa, which would make tab_val_aux R pv w esfss and sfs_val_aux R pv w esf unequal. This doesn’t suggest a flaw in Fitting’s proof, rather that the level of detail he gives doesn’t indicate precisely the sequence of lemmata to be used.
References
Beth, E. (1953). On Padoa’s method in the theory of definition. Indagationes Mathematicae, 15, 330–339.
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.
Dawson, J. E. & Goré, R. (2010). Generic methods for formalising sequent calculi applied to provability logic. In Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning – 17th International Conference, LPAR-17, Yogyakarta, Indonesia (pp. 263–277).
Fitting, M. (1983). Proof Methods for Modal and Intuitionistic Logics. Synthese library. Dordrecht: D. Reidel.
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.
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.
Kripke, S. (1959). A completeness theorem in modal logic. Journal of Symbolic Logic, 24(1), 1–14.
Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg- London-New York: Springer.
Scott, D. (1993). A type-theoretical alternative to ISWIM, CUCH. OWHY. Theoretical Computer Science, 121(1&2), 411–440.
Acknowledgements
We are grateful to the anonymous reviewers for their suggestions for improvements.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Dawson, J.E., Goré, R. (2018). Machine-Checked Meta-theory of Dual-Tableaux for Intuitionistic Logic. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-97879-6_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97878-9
Online ISBN: 978-3-319-97879-6
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)