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