Richard Bornat & Bernard Sufrin (1997):
Jape: A calculator for animating proof-on-paper.
In: CADE-14.
Springer,
pp. 412–415,
doi:10.1007/3-540-63104-6_41.
A. Bundy, D. Basin, D. Hutter & A. Ireland (2005):
Rippling: Meta-level Guidance for Mathematical Reasoning.
Cambridge University Press,
doi:10.1017/CBO9780511543326.
R. Burstall (2000):
ProveEasy: Helping people learn to do proofs.
ENTCS 31(0),
pp. 16 – 32,
doi:10.1016/S1571-0661(05)80327-5.
Lucas Dixon & Jacques D. Fleuriot (2003):
IsaPlanner: A Prototype Proof Planner in Isabelle.
In: CADE-19,
LNCS 2741.
Springer,
pp. 279–283,
doi:10.1007/978-3-540-45085-6_22.
Lucas Dixon & Aleks Kissinger (2010):
Open Graphs and Monoidal Theories.
CoRR abs/1011.4114.
G. Grov, A. Kissinger & Y. Lin (2013):
A Graphical Language for Proof Strategies.
In: LPAR,
LNCS 8312.
Springer Berlin Heidelberg,
pp. 324–339,
doi:10.1007/978-3-642-45221-5_23.
Gudmund Grov & Ewen Maclean (2013):
Towards Automated Proof Strategy Generalisation.
CoRR abs/1303.2975.
Available at http://arxiv.org/abs/1303.2975.
A. Kissinger, A. Merry, L. Dixon, R. Duncan, M. Soloviev & B. Frot (2011):
Quantomatic.
https://sites.google.com/site/quantomatic/.
Helen Lowe & David Duncan (1997):
XBarnacle: Making Theorem Provers More Accessible.
In: CADE1-4.
Springer-Verlag,
pp. 404–408,
doi:10.1007/3-540-63104-6_39.
Colin O'Halloran (2013):
Automated verification of code automatically generated from Simulink..
Automated Software Engineering 20(2),
pp. 237–264,
doi:10.1007/s10515-012-0116-5.
Maris A Ozols, Anthony Cant & Katherine A Eastaughffe (1997):
XIsabelle: A system description.
In: CADE-14.
Springer,
pp. 400–403,
doi:10.1007/3-540-63104-6_38.
Jörg H. Siekmann, Stephan M. Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet & Volker Sorge (1999):
LOUI: Lovely OMEGA User Interface.
Formal Asp. Comput 11(3),
pp. 326–342,
doi:10.1007/s001650050053.