@inbook{6900b965595c4d5c832fcbe5265c65c5,
title = "Machine-Checked Meta-theory of Dual-Tableaux for Intuitionistic Logic",
abstract = "We describe how we formalised the meta-theory of Melvin Fitting{\textquoteright}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.",
author = "Dawson, {Jeremy E.} and Rajeev Gor{\'e}",
note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.",
year = "2018",
doi = "10.1007/978-3-319-97879-6_10",
language = "English",
series = "Outstanding Contributions to Logic",
publisher = "Springer",
pages = "253--282",
booktitle = "Outstanding Contributions to Logic",
address = "Germany",
}