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