David Aspinall, Christoph Lüth & Daniel Winterstein (2007):
A Framework for Interactive Proof.
In: Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference.
Springer-Verlag,
Berlin, Heidelberg,
pp. 161–175,
doi:10.1007/978-3-540-73086-6_15.
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter & Hendrik Spohr (2005):
Cut-Elimination: Experiments with CERES.
In: Franz Baader & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2004,
Lecture Notes in Computer Science 3452.
Springer,
pp. 481–495,
doi:10.1007/978-3-540-32275-7_32.
Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter & Hendrik Spohr (2008):
CERES: An analysis of Fürstenberg's proof of the infinity of primes.
Theor. Comput. Sci. 403(2-3),
pp. 160–175,
doi:10.1016/j.tcs.2008.02.043.
Giuseppe Di Battista, Peter Eades, Roberto Tamassia & Ioannis G Tollis (1994):
Algorithms for drawing graphs: an annotated bibliography.
Computational Geometry 4(5),
pp. 235–282,
doi:10.1016/0925-7721(94)00014-X.
AlanJ. Cain (2010):
Deus ex Machina and the Aesthetics of Proof.
The Mathematical Intelligencer 32(3),
pp. 7–11,
doi:10.1007/s00283-010-9141-z.
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller & Bruno Woltzenlogel-Paleo (2012):
System Feature Description: Importing Refutations into the GAPT Framework.
In: David Pichardie & Tjark Weber: Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012),
CEUR Workshop Proceedings 878,
pp. 51–57.
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller & Bruno Woltzenlogel-Paleo (2013):
ProofTool: a GUI for the GAPT Framework.
In: Cezary Kaliszyk & Christoph Lüth: Proceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012),
Electronic Proceedings in Theoretical Computer Science 118,
pp. 1–14,
doi:10.4204/EPTCS.118.1.
Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia & Daniel Weller (2013):
CERES for First-Order Schemata.
CoRR abs/1303.4257.
Available at http://arxiv.org/abs/1303.4257.
Godfrey Harold Hardy (1940):
A mathematician's apology.
Cambridge University Press.
Stefan Hetzl, Tomer Libal, Martin Riener & Mikheil Rukhaia (2013):
Understanding Resolution Proofs through Herbrand's Theorem.
In: Didier Galmiche & Dominique Larchey-Wendling: Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013),
Lecture Notes in Computer Science 8123,
pp. 157–171,
doi:10.1007/978-3-642-40537-2_15.
Yozo Hida, John O. Lamping & Ramana B. Rao (2005):
Tree visualization system and method based upon a compressed half-plane model of hyperbolic geometry.
Available at http://www.freepatentsonline.com/6901555.html.
Mao Lin Huang, Quang Vinh Nguyen, Wei Lai & Xiaodi Huang (2007):
Three-Dimensional EncCon Tree.
In: Ebad Banissi, Muhammad Sarfraz & Natasha Dejdumrong: CGIV'07: Proceedings of the Computer Graphics, Imaging and Visualisation.
IEEE Computer Society,
pp. 429–433,
doi:10.1109/CGIV.2007.82.
Gérard Huet, Gilles Kahn & Christine Paulin-Mohring (1997):
The Coq Proof Assistant : A Tutorial : Version 6.1.
Rapport de recherche RT-0204.
INRIA.
Projet COQ.
John Lamping, Ramana Rao & Peter Pirolli (1995):
A focus+context technique based on hyperbolic geometry for visualizing large hierarchies.
In: Irvin R. Katz, Robert Mack, Linn Marks, Mary Beth Rosson & Jakob Nielsen: CHI'95: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems.
ACM Press/Addison-Wesley Publishing Co.,
pp. 401–408,
doi:10.1145/223904.223956.
Lars Linsen & Sabine Behrendt (2011):
Linked Treemap: A 3D Treemap-nodelink layout for visualizing hierarchical structures.
Computational Statistics 26(4),
pp. 679–697,
doi:10.1007/s00180-011-0272-2.
John Meier & Clifford A. Reiter (1996):
Fractal representations of Cayley graphs.
Computers and Graphics 20(1),
pp. 163–170,
doi:10.1016/0097-8493(95)00101-8.
Tamara Munzner (1997):
H3: laying out large directed graphs in 3D hyperbolic space.
In: John Dill & Nahum D. Gershon: InfoVis'97: Proceedings of the IEEE Symposium on Information Visualization.
IEEE Computer Society,
pp. 2–10,
doi:10.1109/INFVIS.1997.636718.
Martin Odersky, Lex Spoon & Bill Venners (2010):
Programming in Scala: A Comprehensive Step-by-step Guide,
2nd edition.
Artima, Inc..
Grace D Paterson (2013):
The Aesthetics of Mathematical Proofs.
James Rosindell & Luke J. Harmon (2012):
OneZoom: A Fractal Explorer for the Tree of Life.
PLoS Biology 10(10),
pp. e1001406,
doi:10.1371/journal.pbio.1001406.
Adrian Rusu & Confesor Santiago (2007):
A Practical Algorithm for Planar Straight-line Grid Drawings of General Trees with Linear Area and Arbitrary Aspect Ratio.
In: Ebad Banissi, Remo Aslak Burkhard, Georges Grinstein, Urska Cvek, Marjan Trutschl, Liz Stuart, Theodor G. Wyeld, Gennady Andrienko, Jason Dykes, Mikael Jern, Dennis Groth & Anna Ursyn: IV'07: Proceedings of the International Conference on Information Visualisation.
IEEE Computer Society,
pp. 743–750,
doi:10.1109/IV.2007.14.
H. Schulz (2011):
Treevis.net: A Tree Visualization Reference.
Computer Graphics and Applications, IEEE 31(6),
pp. 11–15,
doi:10.1109/MCG.2011.103.
Ben Shneiderman (1991):
Tree visualization with Tree-maps: A 2-d space-filling approach.
ACM Transactions on Graphics 11,
pp. 92–99,
doi:10.1145/102377.115768.
Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis & Volker Sorge (1998):
A Distributed Graphical User Interface for the Interactive Proof System.
In: Proceedings of the International Workshop "User Interfaces for Theorem Provers 1998 (UITP'98),
Eindhoven, Netherlands,
pp. 130–138.
Available at http://christoph-benzmueller.de/papers/W1.pdf.
John Stasko & Eugene Zhang (2000):
Focus+Context Display and Navigation Techniques for Enhancing Radial, Space-Filling Hierarchy Visualizations.
In: Jock D. Mackinlay, Steven F. Roth & Daniel A. Keim: InfoVis'00: Proceedings of the IEEE Symposium on Information Visualization.
IEEE Computer Society,
pp. 57–65,
doi:10.1109/INFVIS.2000.885091.
G. Sutcliffe (2009):
The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0.
Journal of Automated Reasoning 43(4),
pp. 337–362,
doi:10.1007/s10817-009-9143-8.
Charles Wetherell & Alfred Shannon (1979):
Tidy Drawings of Trees.
IEEE Transactions on Software Engineering SE-5(5),
pp. 514–520,
doi:10.1109/TSE.1979.234212.
W. Windsteiger (2012):
Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System.
In: Cezary Kaliszyk & Christoph Lueth: Proceedings 10th International Workshop On User Interfaces for Theorem Provers, Bremen, Germany, July 11th 2012,
Electronic Proceedings in Theoretical Computer Science 118.
Open Publishing Association,
pp. 72–82,
doi:10.4204/EPTCS.118.5.
Available at http://arxiv.org/abs/1307.1945v1.
Jing Yang, Matthew O. Ward & Elke A. Rundensteiner (2002):
InterRing: An Interactive Tool for Visually Navigating and Manipulating Hierarchical Structures.
In: Pak Chung Wong & Keith Andrews: InfoVis'02: Proceedings of the IEEE Symposium on Information Visualization.
IEEE Computer Society,
pp. 77–84,
doi:10.1109/INFVIS.2002.1173151.
Hee Yong Youn & Adit D. Singh (1988):
Near optimal embedding of binary tree architecture in VLSI.
In: ICDCS'88: Proceedings of the International Conference on Distributed Computing Systems.
IEEE Computer Society,
pp. 86–93,
doi:10.1109/DCS.1988.12503.
eptcs@eptcs.org