@misc(ACMIEEERec13,
 author       = {ACM/IEEE},
 year         = {2013},
 title        = {Computer Science Curricula 2013 --- Curriculum Guidelines for Undergraduate Degree Programs in Computer Science},
 url          = {https://www.acm.org/binaries/content/assets/education/cs2013_web_final.pdf},
)
@article(Anderson1995,
 author       = {J. R. Anderson and A. T. Corbett and K. R. Koedinger and R. Pelletier},
 year         = {1995},
 title        = {Cognitive Tutors: Lessons learned},
 journal      = {J.\ of the Learning Sciences},
 volume       = {4},
 number       = {2},
 pages        = {167--207},
 doi          = {10.1207/s15327809jls0402\_2},
)
@book(Baader:1998:TR:280474,
 author       = {F. Baader and T. Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
 doi          = {10.1017/CBO9781139172752},
)
@incollection(series/faia/BarrettSST09,
 author       = {C. W. Barrett and R. Sebastiani and S. A. Seshia and C. Tinelli},
 year         = {2009},
 title        = {Satisfiability Modulo Theories},
 booktitle    = {Handbook of Satisfiability},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {185},
 publisher    = {IOS Press},
 pages        = {825--885},
 doi          = {10.3233/978-1-58603-929-5-825},
)
@article(DBLP:journals/cj/BornatS99,
 author       = {R. Bornat and B. Sufrin},
 year         = {1999},
 title        = {Animating Formal Proof at the Surface: The Jape Proof Calculator},
 journal      = {Comput. J.},
 volume       = {42},
 number       = {3},
 pages        = {177--192},
 doi          = {10.1093/comjnl/42.3.177},
)
@article(DP60,
 author       = {M. Davis and H. Putnam},
 year         = {1960},
 title        = {A Computing Procedure for Quantification Theory},
 journal      = {J. ACM},
 volume       = {7},
 pages        = {201--215},
 doi          = {10.1145/321033.321034},
)
@inproceedings(DeMoura:2008:ZES:1792734.1792766,
 author       = {De Moura, L. and Bj{\o}rner, N.},
 year         = {2008},
 title        = {Z3: An Efficient SMT Solver},
 booktitle    = {Proc.\ 14th Int.\ Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS'08}},
 series       = {LNCS},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@inproceedings(conf/fmcad/DetersR0BT14,
 author       = {M. Deters and A. Reynolds and T. King and C. W. Barrett and C. Tinelli},
 year         = {2014},
 title        = {A tour of {CVC4}: How it works, and how to use it},
 booktitle    = {Proc.\ 14th Int.\ Conf.\ in Formal Methods in Computer-Aided Design, {FMCAD'14}},
 publisher    = {IEEE},
 pages        = {7},
 doi          = {10.1109/FMCAD.2014.6987586},
)
@inproceedings(Dutertre:cav2014,
 author       = {B. Dutertre},
 year         = {2014},
 title        = {Yices 2.2},
 booktitle    = {Proc.\ 26th Int.\ Conf.\ on Computer Aided Verification, {CAV'14}},
 series       = {LNCS},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {737--744},
 doi          = {10.1007/978-3-319-08867-9\_49},
)
@book(eft_logic_book84,
 author       = {H.-D. Ebbinghaus and J. Flum and W. Thomas},
 year         = {1994},
 title        = {Mathematical Logic},
 edition      = {2nd},
 series       = {Undergraduate Texts in Mathematics},
 publisher    = {Springer},
 address      = {Berlin},
 doi          = {10.1007/978-1-4757-2355-7},
)
@mastersthesis(Ehle17,
 author       = {A. Ehle},
 year         = {2017},
 title        = {Proof Search in the Sequent Calculus for First-Order Logic with Equality},
 school       = {Universit\"{a}t Kassel},
 note         = {Available via \url{https://www.uni-kassel.de/eecs/?id=46992}},
)
@inproceedings(EHL:TTL15,
 author       = {A. Ehle and N. Hundeshagen and M. Lange},
 year         = {2015},
 title        = {The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs},
 booktitle    = {Proc.\ 4th Int.\ Conf.\ on Tools for Teaching Logic, {TTL'15}},
 pages        = {35--44},
 note         = {Available via \url{http://arxiv.org/abs/1507.03666}},
)
@inproceedings(DBLP:conf/ticttl/GasquetSS11a,
 author       = {O. Gasquet and F. Schwarzentruber and M. Strecker},
 year         = {2011},
 title        = {Panda: {A} Proof Assistant in Natural Deduction for All. {A} {G}entzen Style Proof Assistant for Undergraduate Students},
 booktitle    = {Proc.\ 3rd Int.\ Congress on Tools for Teaching Logic, {TICTTL 2011}},
 series       = {LNCS},
 volume       = {6680},
 publisher    = {Springer},
 pages        = {85--92},
 doi          = {10.1007/978-3-642-21350-2\_11},
)
@article(Gentzen35a,
 author       = {G. Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"u}ber das {L}ogische {S}chliessen I},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@phdthesis(Goedel:1930,
 author       = {K. G{\"o}del},
 year         = {1930},
 title        = {{\"U}ber die {V}ollst{\"a}ndigkeit des {L}ogikkalk{\"u}ls},
 school       = {University of Vienna},
)
@misc(GIEmpf16,
 author       = {Gesellschaft f.\ Informatik e.V.},
 year         = {2016},
 title        = {{E}mpfehlungen f{\"u}r {B}achelor- und {M}asterprogramme im {S}tudienfach {I}nformatik an {H}ochschulen},
 url          = {https://www.gi.de/fileadmin/redaktion/empfehlungen/GI-Empfehlungen_Bachelor-Master-Informatik2016.pdf},
)
@article(Jaskowski:1934,
 author       = {S. J{\'a}skowski},
 year         = {1934},
 title        = {On the rules of suppositions in formal logic},
 journal      = {Studia Logica},
 volume       = {1},
 pages        = {5--32},
)
@article(LPT2000,
 author       = {M. J. Lage and G. J. Platt and M. Treglia},
 year         = {2000},
 title        = {Inverting the Classroom: A Gateway to Creating an Inclusive Learning Environment},
 journal      = {J.\ of Economic Education},
 volume       = {31},
 number       = {1},
 pages        = {pp. 30--43},
 doi          = {10.2307/1183338},
)
@article(Robinson65,
 author       = {J. A. Robinson},
 year         = {1965},
 title        = {Machine-oriented logic based on resolution principle},
 journal      = {Journal of the ACM},
 volume       = {12},
 pages        = {23--41},
 doi          = {10.1145/321250.321253},
)
@article(DBLP:journals/ijpp/ShneidermanM79,
 author       = {B. Shneiderman and R. E. Mayer},
 year         = {1979},
 title        = {Syntactic/semantic interactions in programmer behavior: {A} model and experimental results},
 journal      = {Int.\ J.\ of Parallel Programming},
 volume       = {8},
 number       = {3},
 pages        = {219--238},
 doi          = {10.1007/BF00977789},
)
@misc(Stirling97,
 author       = {C. Stirling},
 year         = {1997},
 title        = {Games for bisimulation and model checking},
 note         = {Notes for Mathfit instructional meeting on games and computation, Edinburgh},
)
@book(Szabo1969,
 editor       = {M. E. Szabo},
 year         = {1969},
 title        = {The Collected Papers of Gerhard Gentzen},
 series       = {Studies in Logic and The Foundations of Mathematics},
 publisher    = {North-Holland Publishing Company},
 doi          = {10.2307/2272429},
)
@article(Weber2004,
 author       = {K. Weber and L. Alcock},
 year         = {2004},
 title        = {Semantic and Syntactic Proof Productions},
 journal      = {Educational Studies in Mathematics},
 volume       = {56},
 number       = {2},
 pages        = {209--234},
 doi          = {10.1023/B:EDUC.0000040410.57253.a1},
)