Machine-Checked Meta-theory of Dual-Tableaux for Intuitionistic Logic

  • Jeremy E. Dawson
  • Rajeev GoréEmail author
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)


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.


  1. Beth, E. (1953). On Padoa’s method in the theory of definition. Indagationes Mathematicae, 15, 330–339.CrossRefGoogle Scholar
  2. 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
  3. 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).CrossRefGoogle Scholar
  4. Fitting, M. (1983). Proof Methods for Modal and Intuitionistic Logics. Synthese library. Dordrecht: D. Reidel.CrossRefGoogle Scholar
  5. 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
  6. 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
  7. Kripke, S. (1959). A completeness theorem in modal logic. Journal of Symbolic Logic, 24(1), 1–14.CrossRefGoogle Scholar
  8. Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg- London-New York: Springer.CrossRefGoogle Scholar
  9. Scott, D. (1993). A type-theoretical alternative to ISWIM, CUCH. OWHY. Theoretical Computer Science, 121(1&2), 411–440.CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Research School of Computer ScienceThe Australian National UniversityCanberraAustralia

Personalised recommendations