@inproceedings(Baeta2013,
 author       = {Nuno Baeta and Pedro Quaresma},
 year         = {2013},
 title        = {The full angle method on the {OpenGeoProver}},
 editor       = {Christoph Lange and David Aspinall and Jacques Carette and James Davenport and Andrea Kohlhase and Michael Kohlhase and Paul Libbrecht and Pedro Quaresma and Florian Rabe and Petr Sojka and Iain Whiteside and Wolfgang Windsteiger},
 booktitle    = {{MathUI}, {OpenMath}, {PLMMS} and {ThEdu} Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics},
 series       = {CEUR Workshop Proceedings},
 volume       = {1010},
 address      = {Aachen},
 url          = {http://ceur-ws.org/Vol-1010/paper-08.pdf},
)
@inproceedings(Baeta2019,
 author       = {Nuno Baeta and Pedro Quaresma},
 year         = {2019},
 title        = {Towards Ranking Geometric Automated Theorem Provers},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {30--37},
 doi          = {10.4204/EPTCS.290.3},
)
@inproceedings(Bartocci2019,
 author       = {Ezio Bartocci and Dirk Beyer and Paul~E. Black and Grigory Fedyukovich and Hubert Garavel and Arnd Hartmanns and Marieke Huisman and Fabrice Kordon and Julian Nagele and Mihaela Sighireanu and Bernhard Steffen and Martin Suda and Geoff Sutcliffe and Tjark Weber and Akihisa Yamada},
 year         = {2019},
 title        = {TOOLympics 2019: An Overview of Competitions in Formal Methods},
 editor       = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {11429},
 publisher    = {Springer International Publishing},
 pages        = {3--24},
 doi          = {10.1007/978-3-030-17502-3\_1},
)
@proceedings(toolympics2019,
 editor       = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
 year         = {2019},
 title        = {Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics},
 series       = {LNCS},
 volume       = {11429},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-17462-0},
)
@article(Botana2015,
 author       = {Francisco Botana and Markus Hohenwarter and Jani\v{c}i\'c, Predrag and Zolt\'an Kov\'acs and Ivan Petrovi\'c and Tom\'as Recio and Simon Weitzhofer},
 year         = {2015},
 title        = {{Automated Theorem Proving in GeoGebra: Current Achievements}},
 journal      = {Journal of Automated Reasoning},
 volume       = {55},
 number       = {1},
 pages        = {39--59},
 doi          = {10.1007/s10817-015-9326-4},
)
@article(SWS-AMAI2014,
 author       = {Francisco Botana and Zolt\'an Kov\'acs},
 year         = {2014},
 title        = {A {S}ingular web service for geometric computations},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 pages        = {1--12},
 doi          = {10.1007/s10472-014-9438-2},
)
@incollection(sws-eaca-paper,
 author       = {Francisco Botana and Zolt\'an Kov\'acs and Simon Weitzhofer},
 year         = {2012},
 title        = {Implementing theorem proving in {G}eo{G}ebra by using a {S}ingular webservice},
 booktitle    = {Proceedings EACA 2012, Libro de Res\'umenes del XIII Encuentro de \'Algebra Computacional y Aplicaciones},
 publisher    = {Universidad de Alcal\'a},
 pages        = {67--70},
 url          = {https://www.researchgate.net/publication/277475035_Implementing_Theorem_Proving_in_GeoGebra_by_Using_a_Singular_Webservice},
)
@inproceedings(Braun2018,
 author       = {David Braun and Nicolas Magaud and Pascal Schreck},
 year         = {2018},
 title        = {Formalizing Some ``Small'' Finite Models of Projective Geometry in Coq},
 editor       = {Jacques Fleuriot and Dongming Wang and Jacques Calmet},
 booktitle    = {Artificial Intelligence and Symbolic Computation},
 journal      = {LNCS},
 volume       = {11110},
 pages        = {54--69},
 publisher    = {Springer},
 address      = {Cham},
 doi          = {10.1007/978-3-319-99957-9\_4},
)
@book(Chou1994,
 author       = {Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang},
 year         = {1994},
 title        = {Machine Proofs in Geometry},
 publisher    = {World Scientific},
 doi          = {10.1142/2196},
)
@article(Chou1996a,
 author       = {Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang},
 year         = {1996},
 title        = {Automated Generation of Readable Proofs with Geometric Invariants, I. Multiple and Shortest Proof Generation},
 journal      = {Journal of Automated Reasoning},
 volume       = {17},
 number       = {13},
 pages        = {325--347},
 doi          = {10.1007/BF00283133},
)
@article(Chou1996b,
 author       = {Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang},
 year         = {1996},
 title        = {Automated Generation of Readable Proofs with Geometric Invariants, {II}. Theorem Proving With Full-Angles},
 journal      = {Journal of Automated Reasoning},
 volume       = {17},
 number       = {13},
 pages        = {349--370},
 doi          = {10.1007/BF00283134},
)
@inproceedings(Gao1999,
 author       = {Xiao-Shan Gao},
 year         = {1999},
 title        = {Building Dynamic Mathematical Models with Geometry Expert, III. A Geometry Deductive Database},
 booktitle    = {Proceedings Of ATCM'99},
 publisher    = {ATCM Inc., USA},
 pages        = {153--162},
)
@inproceedings(Gao1998b,
 author       = {Xiao-Shan Gao and C.~C. Zhu and Y.~Huang},
 year         = {1998.},
 title        = {Building Dynamic Mathematical Models with Geometry Expert, II. Linkage},
 editor       = {Z.~B. Li},
 booktitle    = {Proceedings of the Third Asian Symposium on Computer Mathematics},
 publisher    = {LanZhou University Press},
 pages        = {15--22},
)
@article(Gao2004,
 author       = {Xiao-Shan Gao and Qiang Lin},
 year         = {2004},
 title        = {{MMP/G}eometer - A Software Package for Automated Geometric Reasoning},
 journal      = {Lecture Notes in Computer Science},
 volume       = {2930},
 pages        = {44--66},
 doi          = {10.1007/978-3-540-24616-9\_4},
)
@inproceedings(Gao1998a,
 author       = {Xiao-Shan Gao and C.~C. Zhu and Y.~Huang},
 year         = {1998},
 title        = {Building Dynamic Visual and Logic Models with Geometry Expert I},
 editor       = {W.C. Yang},
 booktitle    = {\sl Proceedings of the Third Asian Technology Conference in Mathematics},
 publisher    = {Springer},
 pages        = {216--226},
)
@inproceedings(Geneaux2011,
 author       = {Jean-David G{\'e}nevaux and Julien Narboux and Pascal Schreck},
 year         = {2011},
 title        = {Formalization of Wu's Simple Method in Coq},
 editor       = {Jean-Pierre Jouannaud and Zhong Shao},
 booktitle    = {Certified Programs and Proofs},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {71--86},
 doi          = {10.1007/978-3-642-25379-9\_8},
)
@inproceedings(Gregoire2011,
 author       = {Benjamin Gr{\'e}goire and Lo{\"i}c Pottier and Laurent Th{\'e}ry},
 year         = {2011},
 title        = {Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving},
 editor       = {Thomas Sturm and Christoph Zengler},
 booktitle    = {Automated Deduction in Geometry},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {42--59},
 doi          = {10.1007/978-3-642-21046-4\_3},
)
@incollection(Janicic2006c,
 author       = {Jani{\v c}i{\'c}, Predrag},
 year         = {2006},
 title        = {{GCLC} \begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{—}intopreamble] {A} Tool for Constructive Euclidean Geometry and More Than That},
 editor       = {Andr\'es Iglesias and Nobuki Takayama},
 booktitle    = {Mathematical Software - ICMS 2006},
 series       = {Lecture Notes in Computer Science},
 volume       = {4151},
 publisher    = {Springer},
 pages        = {58--73},
 doi          = {10.1007/11832225\_6},
)
@article(Janicic2012a,
 author       = {Jani\v{c}i\'c, Predrag and Julien Narboux and Pedro Quaresma},
 year         = {2012},
 title        = {The {A}rea {M}ethod: a Recapitulation},
 journal      = {Journal of Automated Reasoning},
 volume       = {48},
 number       = {4},
 pages        = {489--532},
 doi          = {10.1007/s10817-010-9209-7},
)
@inproceedings(Kovacs2015,
 author       = {Zolt{\'a}n Kov{\'a}cs},
 year         = {2015},
 title        = {The {R}elation {T}ool in {G}eo{G}ebra 5},
 editor       = {Francisco Botana and Pedro Quaresma},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Computer Science},
 volume       = {9201},
 publisher    = {Springer},
 pages        = {53--71},
 doi          = {10.1007/978-3-319-21362-0\_4},
)
@incollection(GiacGG-RICAM2013,
 author       = {Zolt\'an Kov\'acs and Bernard Parisse},
 year         = {2015},
 title        = {Giac and {G}eo{G}ebra -- Improved {G}r\"obner Basis Computations},
 editor       = {Jaime Gutierrez and Josef Schicho and Martin Weimann},
 booktitle    = {Computer Algebra and Polynomials},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {126--138},
 doi          = {10.1007/978-3-319-15081-9\_7},
)
@incollection(recio-eaca-paper,
 author       = {Zolt\'an Kov\'acs and Tom\'as Recio and Simon Weitzhofer},
 year         = {2012},
 title        = {Implementing theorem proving in {G}eo{G}ebra by using exact check of a statement in a bounded number of test cases},
 booktitle    = {Proceedings EACA 2012, Libro de Res\'umenes del XIII Encuentro de \'Algebra Computacional y Aplicaciones},
 publisher    = {Universidad de Alcal\'a},
 pages        = {123--126},
 url          = {https://www.researchgate.net/publication/265059624_Implementing_Theorem_Proving_in_GeoGebra_by_Exact_Check_of_a_Statement_in_a_Bounded_Number_of_Test_Cases},
)
@misc(Narboux2009,
 author       = {Julien Narboux},
 year         = {2009},
 title        = {Formalization of the Area Method},
 howpublished = {Coq user contribution},
 note         = {\url{http://dpt-info.u-strasbg.fr/~narboux/area\_method.html}},
)
@article(amai-portfolio,
 author       = {Mladen Nikoli\'c and Vesna Marinkovi\'c and Zolt\'an Kov\'acs and Jani\v{c}i\'c, Predrag},
 year         = {2018},
 title        = {Portfolio theorem proving and prover runtime prediction for geometry},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 pages        = {1--28},
 doi          = {10.1007/s10472-018-9598-6},
)
@misc(Petrovic2012a,
 author       = {Ivan Petrovi{\'{c}} and Jani{\v{c}}i{\'{c}}, Predrag},
 year         = {2012},
 title        = {Integration of {O}penGeoProver with {G}eoGebra},
 url          = {http://argo.matf.bg.ac.rs/events/2012/fatpa2012/slides/IvanPetrovic.pdf},
)
@misc(Pottier1998,
 author       = {Lo\"ic Pottier and Laurent Th\'ery},
 year         = {1998},
 title        = {gbcoq},
 howpublished = {http://www-sop.inria.fr/croap/CFC/Gbcoq.html.},
)
@article(Pottier2008,
 author       = {Lo\IeC{\"\i}c Pottier},
 year         = {2008},
 title        = {Connecting Gr\IeC{\"o}bner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics},
 journal      = {Knowledge Exchange: Automated Provers and Proof Assistants},
 volume       = {418},
 url          = {http://arxiv.org/abs/1007.3615},
)
@incollection(Quaresma2011,
 author       = {Pedro Quaresma},
 year         = {2011},
 title        = {{T}housands of {G}eometric Problems for Geometric {T}heorem {P}rovers ({TGTP})},
 editor       = {Pascal Schreck and Julien Narboux and Richter-Gebert, J{\"u}rgen},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Computer Science},
 volume       = {6877},
 publisher    = {Springer},
 pages        = {169--181},
 doi          = {10.1007/978-3-642-25070-5\_10},
)
@inproceedings(Quaresma2015a,
 author       = {Pedro Quaresma and Nuno Baeta},
 year         = {2015},
 title        = {Current Status of the {I2GATP} Common Format},
 editor       = {Francisco Botana and Pedro Quaresma},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {9201},
 publisher    = {Springer},
 pages        = {119--128},
 doi          = {10.1007/978-3-319-21362-0\_8},
)
@inbook(Quaresma2019a,
 author       = {Pedro Quaresma and Vanda Santos},
 year         = {2019},
 title        = {Proof Technology in Mathematics Research and Teaching},
 chapter      = {Computer-generated geometry proofs in a learning context},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-28483-1},
)
@article(Quaresma2019,
 author       = {Pedro Quaresma and Vanda Santos and Pierluigi Graziani and Nuno Baeta},
 year         = {2019},
 title        = {Taxonomies of geometric problems},
 journal      = {Journal of Symbolic Computation},
 volume       = {97},
 pages        = {31--55},
 publisher    = {Elsevier},
 doi          = {10.1016/j.jsc.2018.12.004},
)
@techreport(Rowe1972,
 author       = {Mary~Budd Rowe},
 year         = {1972},
 title        = {Wait-Time and Rewards as Instructional Variables: Their Influence on Language, Logic, and Fate Control},
 type         = {Technical Report},
 institution  = {National Association for Research in Science Teaching},
 url          = {https://files.eric.ed.gov/fulltext/ED061103.pdf},
)
@techreport(Stahl1994,
 author       = {Robert~J. Stahl},
 year         = {1994},
 title        = {Using ``Think-Time'' and ``Wait-Time'' Skillfully in the Classroom},
 type         = {Technical Report},
 institution  = {ERIC Digest},
 url          = {http://files.eric.ed.gov/fulltext/ED370885.pdf},
)
@incollection(Stojanovic2011,
 author       = {Stojanovi\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{ć}intopreamble], Sana and Pavlovi\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{ć}intopreamble], Vesna and Jani\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{č}intopreamble]i\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{ć}intopreamble], Predrag},
 year         = {2011},
 title        = {A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs},
 editor       = {Pascal Schreck and Julien Narboux and Richter-Gebert, J\IeC{\"u}rgen},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Computer Science},
 volume       = {6877},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {201--220},
 doi          = {10.1007/978-3-642-25070-5\_12},
)
@inproceedings(Stump2014,
 author       = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli},
 year         = {2014},
 title        = {StarExec: A Cross-Community Infrastructure for Logic Solving},
 editor       = {St{\'e}phane Demri and Deepak Kapur and Christoph Weidenbach},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {367--373},
 doi          = {10.1007/978-3-319-08587-6\_28},
)
@inproceedings(Wang2004,
 author       = {Dongming Wang},
 year         = {2004},
 title        = {GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically},
 editor       = {Franz Winkler},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Computer Science},
 volume       = {2930},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {194--215},
 doi          = {10.1007/978-3-540-24616-9\_12},
)
@misc(Wiedijk2000,
 author       = {Freek Wiedijk},
 year         = {2000},
 title        = {The {de Bruijn} factor},
 howpublished = {Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000)},
 note         = {Portland, Oregon, USA, 14-18 August 2000},
)
@inbook(Wu1984,
 author       = {Wen-Tsun Wu},
 year         = {1984},
 title        = {Automated Theorem Proving: After 25 Years},
 chapter      = {On the decision problem and the mechanization of theorem proving in elementary geometry},
 pages        = {213--234},
 series       = {Contemporary Mathematics},
 volume       = {29},
 publisher    = {American Mathematical Society},
 doi          = {10.1090/conm/029/12},
)
@incollection(Ye2011,
 author       = {Zheng Ye and Shang-Ching Chou and Xiao-Shan Gao},
 year         = {2011},
 title        = {An Introduction to Java Geometry Expert},
 editor       = {Thomas Sturm and Christoph Zengler},
 booktitle    = {Automated Deduction in Geometry},
 series       = {Lecture Notes in Computer Science},
 volume       = {6301},
 publisher    = {Springer},
 address      = {Berlin Heidelberg},
 pages        = {189--195},
 doi          = {10.1007/978-3-642-21046-4\_10},
)