%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Larry Paulson at 2021-02-01 11:31:03 +0000 


%% Saved with string encoding Unicode (UTF-8) 



@article{Poincare_Disc-AFP,
	author = {Danijela Simi{\'c} and Filip Mari{\'c} and Pierre Boutry},
	date-added = {2021-02-01 11:30:15 +0000},
	date-modified = {2021-02-01 11:30:15 +0000},
	issn = {2150-914x},
	journal = {Archive of Formal Proofs},
	month = dec,
	note = {\url{https://isa-afp.org/entries/Poincare_Disc.html}, Formal proof development},
	title = {Poincar{\'e} Disc Model},
	year = 2019}

@article{Tarskis_Geometry-AFP,
	author = {T. J. M. Makarios},
	date-added = {2021-02-01 11:28:01 +0000},
	date-modified = {2021-02-01 11:28:28 +0000},
	issn = {2150-914x},
	journal = {Archive of Formal Proofs},
	month = oct,
	note = {\url{https://isa-afp.org/entries/Tarskis_Geometry.html}, Formal proof development},
	title = {The Independence of {Tarski's Euclidean} Axiom},
	year = 2012}

@book{tarski,
	address = {Berlin},
	author = {Wolfram Schwabh{\"a}user and Wanda Szmielew and Alfred Tarski},
	publisher = {Springer-Verlag},
	title = {{Metamathematische Methoden in der Geometrie}},
	year = {1983}}

@mastersthesis{makarios,
	author = {Makarios, Timothy James McKenzie},
	note = {Master Thesis},
	school = {Victoria University of Wellington},
	title = {{A Mechanical Verification of the Independence of Tarski's Euclidean Axiom}},
	year = {2012}}

@misc{beeson:hal-01912024,
	author = {Beeson, Michael and Boutry, Pierre and Braun, Gabriel and Gries, Charly and Narboux, Julien},
	hal_id = {hal-01912024},
	hal_version = {v1},
	keywords = {coordinates ; Triangle centers ; parallel postulates ; Euclidean geometry ; Formal proofs ; Coq Proof Assistant ; Foundations of geometry ; arithmetization ; Thales theorem ; pythagoras theorem ; neutral geometry ; Tarski's geometry ; Hilbert's geometry},
	month = Jun,
	title = {{GeoCoq}},
	url = {https://hal.inria.fr/hal-01912024},
	year = {2018},
	Bdsk-Url-1 = {https://hal.inria.fr/hal-01912024}}

@article{wiedijk2012synthesis,
	author = {Wiedijk, Freek},
	journal = {Logical Methods in Computer Science},
	publisher = {Episciences. org},
	title = {A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving},
	volume = {8},
	year = {2012}}

@article{boutry:hal-01178236,
	author = {Boutry, Pierre and Gries, Charly and Narboux, Julien and Schreck, Pascal},
	doi = {10.1007/s10817-017-9422-8},
	hal_id = {hal-01178236},
	hal_version = {v2},
	journal = {{Journal of Automated Reasoning}},
	keywords = {Archimedes' axiom ; axiom ; Aristotle's ; Coq ; neutral geometry ; formalization ; decidability of intersection ; classification ; foundations of geometry ; Euclid ; parallel postulate ; Saccheri-Legendre theorem ; sum of angles},
	note = {online first},
	pages = {68},
	pdf = {https://hal.inria.fr/hal-01178236/file/parallel_postulates_revised.pdf},
	publisher = {{Springer Verlag}},
	title = {{Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq}},
	url = {https://hal.inria.fr/hal-01178236},
	year = {2017},
	Bdsk-Url-1 = {https://hal.inria.fr/hal-01178236},
	Bdsk-Url-2 = {https://doi.org/10.1007/s10817-017-9422-8}}

@inproceedings{gries:hal-01228612,
	address = {Saint Malo, France},
	author = {Gries, Charly and Boutry, Pierre and Narboux, Julien},
	booktitle = {{Les vingt-septi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2016)}},
	hal_id = {hal-01228612},
	hal_version = {v2},
	keywords = {Euclid ; formalization ; Coq ; parallel postulate ; geometry ; formalisation},
	month = Jan,
	organization = {{Jade Algave and Julien Signoles}},
	pages = {15},
	pdf = {https://hal.inria.fr/hal-01228612/file/jfla2016-gries-boutry-narboux.pdf},
	series = {Actes des Vingt-septi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2016)},
	title = {{Somme des angles d'un triangle et unicit{\'e} de la parall{\`e}le : une preuve d'{\'e}quivalence formalis{\'e}e en Coq}},
	url = {https://hal.inria.fr/hal-01228612},
	year = {2016},
	Bdsk-Url-1 = {https://hal.inria.fr/hal-01228612}}

@inproceedings{narboux:inria-00118812,
	address = {Pontevedra, Spain},
	author = {Narboux, Julien},
	booktitle = {{Automated Deduction in Geometry 2006}},
	doi = {10.1007/978-3-540-77356-6},
	editor = {Eugenio Roanes Lozano, Francisco Botana},
	hal_id = {inria-00118812},
	hal_version = {v1},
	keywords = {Tarski's axioms ; Coq ; Formal Proof ; geometry},
	month = Aug,
	organization = {{Francisco Botana}},
	pages = {139-156},
	pdf = {https://hal.inria.fr/inria-00118812/file/adg06-narboux.pdf},
	publisher = {{Springer}},
	series = {LNCS},
	title = {{Mechanical Theorem Proving in Tarski's geometry.}},
	url = {https://hal.inria.fr/inria-00118812},
	volume = {4869},
	year = {2006},
	Bdsk-Url-1 = {https://hal.inria.fr/inria-00118812},
	Bdsk-Url-2 = {https://doi.org/10.1007/978-3-540-77356-6}}

@article{boutry:hal-01483457,
	author = {Boutry, Pierre and Braun, Gabriel and Narboux, Julien},
	doi = {10.1016/j.jsc.2018.04.007},
	hal_id = {hal-01483457},
	hal_version = {v1},
	journal = {{Journal of Symbolic Computation}},
	keywords = {Pythagoras' theorem ; intercept theorem ; arithmetization ; Coq ; geometry ; Formalization ; area method},
	pages = {149-168},
	pdf = {https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf},
	publisher = {{Elsevier}},
	series = {Special Issue on Symbolic Computation in Software Science},
	title = {{Formalization of the Arithmetization of Euclidean Plane Geometry and Applications}},
	url = {https://hal.inria.fr/hal-01483457},
	volume = {90},
	year = {2019},
	Bdsk-Url-1 = {https://hal.inria.fr/hal-01483457},
	Bdsk-Url-2 = {https://doi.org/10.1016/j.jsc.2018.04.007}}

@incollection{narboux:hal-01779452,
	author = {Narboux, Julien and Janicic, Predrag and Fleuriot, Jacques},
	booktitle = {{Handbook of Geometric Constraint Systems Principles}},
	editor = {Meera Sitharam and Audrey St. John and Jessica Sidman},
	hal_id = {hal-01779452},
	hal_version = {v1},
	publisher = {{Chapman and Hall/CRC }},
	series = {Discrete Mathematics and Its Applications},
	title = {{Computer-assisted Theorem Proving in Synthetic Geometry}},
	url = {https://hal.inria.fr/hal-01779452},
	year = {2018},
	Bdsk-Url-1 = {https://hal.inria.fr/hal-01779452}}

@article{dhurdjevic2015automated,
	author = {{\DH}ur{\dj}evi{\'c}, Sana Stojanovi{\'c} and Narboux, Julien and Jani{\v{c}}i{\'c}, Predrag},
	journal = {Annals of Mathematics and Artificial Intelligence},
	number = {3-4},
	pages = {249--269},
	publisher = {Springer},
	title = {Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry},
	volume = {74},
	year = {2015}}

@inproceedings{beeson2014otter,
	author = {Beeson, Michael and Wos, Larry},
	booktitle = {International Joint Conference on Automated Reasoning},
	organization = {Springer},
	pages = {495--510},
	title = {OTTER proofs in Tarskian geometry},
	year = {2014}}

@inproceedings{DBLP:conf/csedu/DoreB18a,
	author = {Maximilian Dor{\'{e}} and Krysia Broda},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/conf/csedu/DoreB18a.bib},
	booktitle = {Computer Supported Education - 10th International Conference, {CSEDU} 2018, Funchal, Madeira, Portugal, March 15-17, 2018, Revised Selected Papers},
	doi = {10.1007/978-3-030-21151-6\_26},
	editor = {Bruce M. McLaren and Rob Reilly and Susan Zvacek and James Uhomoibhi},
	pages = {549--571},
	publisher = {Springer},
	series = {Communications in Computer and Information Science},
	timestamp = {Tue, 25 Jun 2019 19:08:13 +0200},
	title = {Intuitive Reasoning in Formalized Mathematics with Elfe},
	url = {https://doi.org/10.1007/978-3-030-21151-6\_26},
	volume = {1022},
	year = {2018},
	Bdsk-Url-1 = {https://doi.org/10.1007/978-3-030-21151-6%5C_26}}

@article{DBLP:journals/fm/CoghettoG19,
	author = {Roland Coghetto and Adam Grabowski},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/fm/CoghettoG19.bib},
	doi = {10.2478/forma-2019-0008},
	journal = {Formalized Mathematics},
	number = {1},
	pages = {75--85},
	timestamp = {Mon, 17 Jun 2019 17:02:00 +0200},
	title = {Tarski Geometry Axioms. Part {IV} - Right Angle},
	url = {https://doi.org/10.2478/forma-2019-0008},
	volume = {27},
	year = {2019},
	Bdsk-Url-1 = {https://doi.org/10.2478/forma-2019-0008}}

@article{DBLP:journals/fm/CoghettoG17,
	author = {Roland Coghetto and Adam Grabowski},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/fm/CoghettoG17.bib},
	doi = {10.1515/forma-2017-0028},
	journal = {Formalized Mathematics},
	number = {4},
	pages = {289--313},
	timestamp = {Sat, 19 Oct 2019 19:33:25 +0200},
	title = {Tarski Geometry Axioms. Part {III}},
	url = {https://doi.org/10.1515/forma-2017-0028},
	volume = {25},
	year = {2017},
	Bdsk-Url-1 = {https://doi.org/10.1515/forma-2017-0028}}

@article{DBLP:journals/fm/CoghettoG16,
	author = {Roland Coghetto and Adam Grabowski},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/fm/CoghettoG16.bib},
	doi = {10.1515/forma-2016-0012},
	journal = {Formalized Mathematics},
	number = {2},
	pages = {157--166},
	timestamp = {Sat, 19 Oct 2019 19:33:25 +0200},
	title = {Tarski Geometry Axioms - Part {II}},
	url = {https://doi.org/10.1515/forma-2016-0012},
	volume = {24},
	year = {2016},
	Bdsk-Url-1 = {https://doi.org/10.1515/forma-2016-0012}}

@article{DBLP:journals/fm/RichterGA14,
	author = {William Richter and Adam Grabowski and Jesse Alama},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	biburl = {https://dblp.org/rec/journals/fm/RichterGA14.bib},
	journal = {Formalized Mathematics},
	number = {2},
	pages = {167--176},
	timestamp = {Thu, 19 Feb 2015 15:03:13 +0100},
	title = {Tarski Geometry Axioms},
	url = {http://www.degruyter.com/view/j/forma.2014.22.issue-2/forma-2014-0017/forma-2014-0017.xml},
	volume = {22},
	year = {2014},
	Bdsk-Url-1 = {http://www.degruyter.com/view/j/forma.2014.22.issue-2/forma-2014-0017/forma-2014-0017.xml}}

@article{sutcliffe1998tptp,
	author = {Sutcliffe, Geoff and Suttner, Christian},
	journal = {Journal of Automated Reasoning},
	number = {2},
	pages = {177--203},
	publisher = {Springer},
	title = {The TPTP problem library},
	volume = {21},
	year = {1998}}

@book{martin2012foundations,
	author = {Martin, George Edward},
	publisher = {Springer Science \& Business Media},
	title = {The foundations of geometry and the non-Euclidean plane},
	year = {2012}}

@inproceedings{nipkow2002structured,
	author = {Nipkow, Tobias},
	booktitle = {International Workshop on Types for Proofs and Programs},
	organization = {Springer},
	pages = {259--278},
	title = {Structured proofs in Isar/HOL},
	year = {2002}}

@article{PoincareDisc,
	author = {Simic, Danijela and Maric, Filip and Boutry, Pierre},
	doi = {10.1007/s10817-020-09551-2},
	journal = {J. Autom. Reasoning},
	number = {4},
	title = {Formalization of the Poincar{\'e} Disc Model of Hyperbolic Geometry},
	url = {https://doi.org/10.1007/s10817-020-09551-2},
	volume = {64},
	year = {2020},
	Bdsk-Url-1 = {https://doi.org/10.1007/s10817-020-09551-2}}

@inproceedings{stojanovic2010coherent,
	author = {Stojanovi{\'c}, Sana and Pavlovi{\'c}, Vesna and Jani{\v{c}}i{\'c}, Predrag},
	booktitle = {International Workshop on Automated Deduction in Geometry},
	organization = {Springer},
	pages = {201--220},
	title = {A coherent logic based geometry theorem prover capable of producing formal and readable proofs},
	year = {2010}}

@article{beeson2017finding,
	author = {Beeson, Michael and Wos, Larry},
	journal = {Journal of Automated Reasoning},
	number = {1},
	pages = {181--207},
	publisher = {Springer},
	title = {Finding proofs in Tarskian geometry},
	volume = {58},
	year = {2017}}

@article{beeson2019proof,
	author = {Beeson, Michael and Narboux, Julien and Wiedijk, Freek},
	journal = {Annals of Mathematics and Artificial Intelligence},
	number = {2},
	pages = {213--257},
	publisher = {Springer},
	title = {Proof-checking Euclid},
	volume = {85},
	year = {2019}}

@article{narboux2018computer,
	author = {Narboux, Julien and Janicic, Predrag and Fleuriot, Jacques},
	journal = {Handbook of Geometric Constraint Systems Principles},
	pages = {25--73},
	publisher = {Chapman and Hall/CRC},
	title = {Computer-assisted theorem proving in synthetic geometry},
	year = {2018}}

@phdthesis{boutry2018formalization,
	author = {Boutry, Pierre},
	school = {Universit{\'e} de Strasbourg},
	title = {On the formalization of foundations of geometry},
	year = {2018}}
