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

%% Created for Anthony Bordg at 2018-06-14 11:19:05 +0100 


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



@article{Magaud_2012,
	Author = {Magaud, Nicolas and Narboux, Julien and Schreck, Pascal},
	Date-Added = {2018-06-12 11:11:19 +0000},
	Date-Modified = {2018-06-12 11:11:19 +0000},
	Doi = {10.1016/j.comgeo.2010.06.004},
	Issn = {0925-7721},
	Journal = {Computational Geometry},
	Month = {Oct},
	Number = {8},
	Pages = {406--424},
	Publisher = {Elsevier BV},
	Title = {A case study in formalizing projective geometry in Coq: Desargues theorem},
	Url = {https://doi.org/10.1016/j.comgeo.2010.06.004},
	Volume = {45},
	Year = {2012},
	Bdsk-File-1 = { }}
	
@Article{Bezem2008,
author="Bezem, Marc
and Hendriks, Dimitri",
title="On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic",
journal="Journal of Automated Reasoning",
year="2008",
month="Jan",
day="01",
volume="40",
number="1",
pages="61--85",
abstract="We propose to combine interactive proof construction with proof automation for a fragment of first-order logic called Coherent Logic (CL). CL allows enough existential quantification to make Skolemization unnecessary. Moreover, CL has a constructive proof system based on forward reasoning, which is easy to automate and where standardized proof objects can easily be obtained. We have implemented in Prolog a CL prover which generates Coq proof scripts. We test our approach with a case study: Hessenberg's Theorem, which states that in elementary projective plane geometry Pappus' Axiom implies Desargues' Axiom. Our CL prover makes it possible to automate large parts of the proof, in particular taking care of the large number of degenerate cases.",
issn="1573-0670",
doi="10.1007/s10817-007-9086-x",
url="https://doi.org/10.1007/s10817-007-9086-x"
}

@book{coxeter2003projective,
  title={Projective Geometry},
  author={Coxeter, H.S.M.},
  isbn={9780387406237},
  lccn={87009750},
  year={2003},
  publisher={Springer New York}
}

	
