1. ACM/IEEE (2013): Computer Science Curricula 2013 — Curriculum Guidelines for Undergraduate Degree Programs in Computer Science. Available at
  2. J. R. Anderson, A. T. Corbett, K. R. Koedinger & R. Pelletier (1995): Cognitive Tutors: Lessons learned. J. of the Learning Sciences 4(2), pp. 167–207, doi:10.1207/s15327809jls0402_2.
  3. F. Baader & T. Nipkow (1998): Term Rewriting and All That. Cambridge University Press, New York, NY, USA, doi:10.1017/CBO9781139172752.
  4. C. W. Barrett, R. Sebastiani, S. A. Seshia & C. Tinelli (2009): Satisfiability Modulo Theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications 185. IOS Press, pp. 825–885, doi:10.3233/978-1-58603-929-5-825.
  5. R. Bornat & B. Sufrin (1999): Animating Formal Proof at the Surface: The Jape Proof Calculator. Comput. J. 42(3), pp. 177–192, doi:10.1093/comjnl/42.3.177.
  6. M. Davis & H. Putnam (1960): A Computing Procedure for Quantification Theory. J. ACM 7, pp. 201–215, doi:10.1145/321033.321034.
  7. L. De Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08, LNCS. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  8. M. Deters, A. Reynolds, T. King, C. W. Barrett & C. Tinelli (2014): A tour of CVC4: How it works, and how to use it. In: Proc. 14th Int. Conf. in Formal Methods in Computer-Aided Design, FMCAD'14. IEEE, pp. 7, doi:10.1109/FMCAD.2014.6987586.
  9. B. Dutertre (2014): Yices 2.2. In: Proc. 26th Int. Conf. on Computer Aided Verification, CAV'14, LNCS 8559. Springer, pp. 737–744, doi:10.1007/978-3-319-08867-9_49.
  10. H.-D. Ebbinghaus, J. Flum & W. Thomas (1994): Mathematical Logic, 2nd edition, Undergraduate Texts in Mathematics. Springer, Berlin, doi:10.1007/978-1-4757-2355-7.
  11. A. Ehle (2017): Proof Search in the Sequent Calculus for First-Order Logic with Equality. Universität Kassel. Available via
  12. A. Ehle, N. Hundeshagen & M. Lange (2015): The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs. In: Proc. 4th Int. Conf. on Tools for Teaching Logic, TTL'15, pp. 35–44. Available via
  13. O. Gasquet, F. Schwarzentruber & M. Strecker (2011): Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students. In: Proc. 3rd Int. Congress on Tools for Teaching Logic, TICTTL 2011, LNCS 6680. Springer, pp. 85–92, doi:10.1007/978-3-642-21350-2_11.
  14. G. Gentzen (1935): Untersuchungen über das Logische Schliessen I. Mathematische Zeitschrift 39, pp. 176–210, doi:10.1007/BF01201353.
  15. K. Gödel (1930): Über die Vollständigkeit des Logikkalküls. University of Vienna.
  16. Gesellschaft f. Informatik e.V. (2016): Empfehlungen für Bachelor- und Masterprogramme im Studienfach Informatik an Hochschulen. Available at
  17. S. Jáskowski (1934): On the rules of suppositions in formal logic. Studia Logica 1, pp. 5–32.
  18. M. J. Lage, G. J. Platt & M. Treglia (2000): Inverting the Classroom: A Gateway to Creating an Inclusive Learning Environment. J. of Economic Education 31(1), pp. pp. 30–43, doi:10.2307/1183338.
  19. J. A. Robinson (1965): Machine-oriented logic based on resolution principle. Journal of the ACM 12, pp. 23–41, doi:10.1145/321250.321253.
  20. B. Shneiderman & R. E. Mayer (1979): Syntactic/semantic interactions in programmer behavior: A model and experimental results. Int. J. of Parallel Programming 8(3), pp. 219–238, doi:10.1007/BF00977789.
  21. C. Stirling (1997): Games for bisimulation and model checking. Notes for Mathfit instructional meeting on games and computation, Edinburgh.
  22. M. E. Szabo (1969): The Collected Papers of Gerhard Gentzen. Studies in Logic and The Foundations of Mathematics. North-Holland Publishing Company, doi:10.2307/2272429.
  23. K. Weber & L. Alcock (2004): Semantic and Syntactic Proof Productions. Educational Studies in Mathematics 56(2), pp. 209–234, doi:10.1023/B:EDUC.0000040410.57253.a1.

Comments and questions to:
For website issues: