@article(andreoli1992logic,
 author       = {Jean{-}Marc Andreoli},
 year         = {1992},
 title        = {Logic Programming with Focusing Proofs in Linear Logic},
 journal      = {J. Log. Comput.},
 volume       = {2},
 number       = {3},
 pages        = {297--347},
 doi          = {10.1093/logcom/2.3.297},
)
@article(BaazL92,
 author       = {Matthias Baaz and Alexander Leitsch},
 year         = {1992},
 title        = {Complexity of Resolution Proofs and Function Introduction},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {57},
 number       = {3},
 pages        = {181--215},
 doi          = {10.1016/0168-0072(92)90042-X},
)
@article(balsiger2000benchmark,
 author       = {Peter Balsiger and Alain Heuerding and Stefan Schwendimann},
 year         = {2000},
 title        = {A Benchmark Method for the Propositional Modal Logics K, KT, {S4}},
 journal      = {J. Autom. Reasoning},
 volume       = {24},
 number       = {3},
 pages        = {297--317},
 doi          = {10.1023/A:1006249507577},
)
@article(Beckert97a,
 author       = {Bernhard Beckert and Rajeev Gor{\'{e}}},
 year         = {2001},
 title        = {Free-Variable Tableaux for Propositional Modal Logics},
 journal      = {Studia Logica},
 volume       = {69},
 number       = {1},
 pages        = {59--96},
 doi          = {10.1023/A:1013886427723},
)
@incollection(BlaVBe07,
 author       = {Patrick Blackburn and Van Benthem, Johan},
 year         = {2007},
 title        = {{Modal logic: a Semantic Perspective}},
 editor       = {Frank Wolter Patrick Blackburn, Johan van Benthem},
 booktitle    = {{Handbook of Modal Logic}},
 publisher    = {{Elsevier}},
 pages        = {1--82},
 doi          = {10.1016/S1570-2464(07)80004-8},
)
@inproceedings(boespflug2012lambdapi,
 author       = {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant},
 year         = {2012},
 title        = {The $\lambda$$\Pi$-calculus modulo as a universal proof language},
 booktitle    = {the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012)},
 volume       = {878},
 pages        = {pp--28},
)
@inproceedings(cauderlier2015checking,
 author       = {Rapha{\"{e}}l Cauderlier and Pierre Halmagrand},
 year         = {2015},
 title        = {Checking Zenon Modulo Proofs in Dedukti},
 editor       = {Cezary Kaliszyk and Andrei Paskevich},
 booktitle    = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015.},
 series       = {{EPTCS}},
 volume       = {186},
 pages        = {57--73},
 doi          = {10.4204/EPTCS.186.7},
)
@incollection(chihaniLR15,
 author       = {Zakaria Chihani and Tomer Libal and Giselle Reis},
 year         = {2015},
 title        = {The Proof Certifier Checkers},
 editor       = {Hans de Nivelle},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, {TABLEAUX} 2015, Wroc{\l}aw, Poland, September 21-24, 2015. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9323},
 publisher    = {Springer},
 pages        = {201--210},
 doi          = {10.1007/978-3-319-24312-2\_14},
)
@article(fitting1972tableau,
 author       = {Melvin Fitting},
 year         = {1972},
 title        = {Tableau methods of proof for modal logics},
 journal      = {Notre Dame Journal of Formal Logic},
 volume       = {13},
 number       = {2},
 pages        = {237--247},
 doi          = {10.1305/ndjfl/1093894722},
)
@incollection(Fit07,
 author       = {Melvin Fitting},
 year         = {2007},
 title        = {{Modal proof theory}},
 editor       = {Patrick Blackburn and Johan van Benthem and Frank Wolter},
 booktitle    = {{Handbook of Modal Logic}},
 publisher    = {{Elsevier}},
 pages        = {85--138},
 doi          = {10.1016/S1570-2464(07)80005-X},
)
@article(Fit12,
 author       = {Melvin Fitting},
 year         = {2012},
 title        = {Prefixed tableaus and nested sequents},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {163},
 number       = {3},
 pages        = {291--313},
 doi          = {10.1016/j.apal.2011.09.004},
)
@book(Gab96,
 author       = {Dov M. Gabbay},
 year         = {1996},
 title        = {Labelled Deductive Systems},
 publisher    = {Clarendon Press},
)
@article(LiaMil09,
 author       = {Chuck Liang and Dale Miller},
 year         = {2009},
 title        = {Focusing and polarization in linear, intuitionistic, and classical logics},
 journal      = {Theor. Comput. Sci.},
 volume       = {410},
 number       = {46},
 pages        = {4747--4768},
 doi          = {10.1016/j.tcs.2009.07.041},
)
@inproceedings(MarMilVol16,
 author       = {Sonia Marin and Dale Miller and Marco Volpe},
 year         = {2016},
 title        = {A focused framework for emulating modal proof systems},
 booktitle    = {Proceedings of the 11th International Conference on Advances in Modal Logic, Budapest, 30 August - 2 September 2016},
 note         = {To appear},
)
@unpublished(erc,
 author       = {Dale Miller},
 year         = {2011},
 title        = {ProofCert: Broad Spectrum Proof Certificates},
 note         = {An ERC Advanced Grant funded for the five years 2012-2016},
)
@book(Miller2012,
 author       = {Dale Miller and Gopalan Nadathur},
 year         = {2012},
 title        = {Programming with Higher-Order Logic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139021326},
 url          = {http://www.cambridge.org/de/academic/subjects/computer- science/programming-languages-and-applied-logic/programming- higher-order-logic?format=HB},
)
@inproceedings(MilVol15,
 author       = {Dale Miller and Marco Volpe},
 year         = {2015},
 title        = {Focused Labeled Proof Systems for Modal Logic},
 editor       = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9450},
 publisher    = {Springer},
 pages        = {266--280},
 doi          = {10.1007/978-3-662-48899-7\_19},
)
@article(Neg05,
 author       = {Sara Negri},
 year         = {2005},
 title        = {Proof Analysis in Modal Logic},
 journal      = {J. Philosophical Logic},
 volume       = {34},
 number       = {5-6},
 pages        = {507--544},
 doi          = {10.1007/s10992-005-2267-3},
)
@inproceedings(Ohlbach1988,
 author       = {Hans J{\"{u}}rgen Ohlbach},
 year         = {1988},
 title        = {A Resolution Calculus for Modal Logics},
 editor       = {Ewing L. Lusk and Ross A. Overbeek},
 booktitle    = {9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {310},
 publisher    = {Springer},
 pages        = {500--516},
 doi          = {10.1007/BFb0012852},
)
@inproceedings(reeves1987semantic,
 author       = {Steve Reeves},
 year         = {1987},
 title        = {Semantic Tableaux As a Framework for Automated Theorem-proving},
 booktitle    = {On Advances in Artificial Intelligence},
 publisher    = {John Wiley \& Sons, Inc.},
 address      = {New York, NY, USA},
 pages        = {125--139},
 url          = {http://dl.acm.org/citation.cfm?id=29992.30001},
)
@article(Robinson1965,
 author       = {John Alan Robinson},
 year         = {1965},
 title        = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal      = {J. {ACM}},
 volume       = {12},
 number       = {1},
 pages        = {23--41},
 doi          = {10.1145/321250.321253},
)