1. 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.
  2. 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.
  3. 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.
  4. Bernhard Beckert & Rajeev Goré (2001): Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69(1), pp. 59–96, doi:10.1023/A:1013886427723.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. Dov M. Gabbay (1996): Labelled Deductive Systems. Clarendon Press.
  13. 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.
  14. 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.
  15. Dale Miller (2011): ProofCert: Broad Spectrum Proof Certificates. An ERC Advanced Grant funded for the five years 2012-2016.
  16. Dale Miller & Gopalan Nadathur (2012): Programming with Higher-Order Logic. Cambridge University Press, doi:10.1017/CBO9781139021326. Available at science/programming-languages-and-applied-logic/programming- higher-order-logic?format=HB.
  17. 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.
  18. Sara Negri (2005): Proof Analysis in Modal Logic. J. Philosophical Logic 34(5-6), pp. 507–544, doi:10.1007/s10992-005-2267-3.
  19. 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.
  20. 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
  21. 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.

Comments and questions to:
For website issues: