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.
F. Baader & T. Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
New York, NY, USA,
doi:10.1017/CBO9781139172752.
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.
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.
M. Davis & H. Putnam (1960):
A Computing Procedure for Quantification Theory.
J. ACM 7,
pp. 201–215,
doi:10.1145/321033.321034.
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.
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.
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.
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.
A. Ehle (2017):
Proof Search in the Sequent Calculus for First-Order Logic with Equality.
Universität Kassel.
Available via https://www.uni-kassel.de/eecs/?id=46992.
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 http://arxiv.org/abs/1507.03666.
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.
G. Gentzen (1935):
Untersuchungen über das Logische Schliessen I.
Mathematische Zeitschrift 39,
pp. 176–210,
doi:10.1007/BF01201353.
K. Gödel (1930):
Über die Vollständigkeit des Logikkalküls.
University of Vienna.
S. Jáskowski (1934):
On the rules of suppositions in formal logic.
Studia Logica 1,
pp. 5–32.
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.
J. A. Robinson (1965):
Machine-oriented logic based on resolution principle.
Journal of the ACM 12,
pp. 23–41,
doi:10.1145/321250.321253.
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.
C. Stirling (1997):
Games for bisimulation and model checking.
Notes for Mathfit instructional meeting on games and computation, Edinburgh.
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.
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.
eptcs@eptcs.org