@PREAMBLE{ {\newcommand{\noopsort}[1]{} \newcommand{\singleletter}[1]{#1} } }
@STRING{ ADW = {Addison-Wesley} }
@STRING{ AMS = {American Mathematical Society} }

@PhdThesis{Chou85,
author = {Shang-Ching Chou},
title = {Proving and discovering geometry theorems using Wu's method},
school = {The University of Texas},
year = {1985},
address = {Austin},
month = {December}
}

@Book{chou88,
  author =       {Shang-Ching Chou},
  title =        {Mechanical Geometry Theorem Proving},
  publisher =    {D.~Reidel Publishing Company},
  year =         {1988}
}

@inproceedings{Chou93,
   author    = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong},
   editor    = {Vardi, Moshe},
   title     = {Automated production of traditional proofs for constructive
       geometry theorems},
   booktitle = {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science {LICS}},
   pages     = {48--56},
   year      = {1993},
   month     = {June},
   publisher = {IEEE Computer Society Press}
}

@Book{Chou94,
  author =       {Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang},
  title =        {Machine Proofs in Geometry},
  publisher =    {World Scientific},
  year =         {1994},
  address =      {Singapore}
}

@article{Chou95a,
   author    = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong},
   title     = {Automated Production of Traditional Proofs in Solid Geometry},
   journal   = {Journal of Automated Reasoning},
   pages     = {257--291},
   year      = {1995},
   volume    = {14}
}

@article{Chou96,
   author    = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong},
   title     = {Automated Generation of Readable Proofs with Geometric Invariants, {I}. Multiple and Shortest Proof Generation},
   journal   = {Journal of Automated Reasoning},
   pages     = {325-347},
   year      = {1996},
   volume    = {17}
}

@article{Chou96a,
   author    = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong},
   title     = {Automated Generation of Readable Proofs with Geometric Invariants, {II}. Theorem Proving With Full-Angles},
   journal   = {Journal of Automated Reasoning},
   pages     = {349-370},
   year      = {1996},
   volume    = {17}
}

@ARTICLE{Coelho86,
  author = {Coelho, H. and Pereira, L. M.},
  title = {Automated reasoning in geometry theorem proving with {P}rolog},
  journal = {Journal of Automated Reasoning},
  year = {1986},
  volume = {2},
  pages = {329--390},
  number = {4},
}

@TECHREPORT{Goldstein73,
  author = {Goldstein, Ira},
  title = {Elementary {G}eometry {T}heorem {P}roving},
  institution = {MIT},
  year = {1973},
  type = {AI Lab memo},
  number = {280},
  month = {April}
}

@INPROCEEDINGS{Janicic06a,
  author = {Jani{\v c}i{\'c}, Predrag and Quaresma, Pedro},
  title = {System Description: GCLCprover + GeoThms},
  booktitle = {IJCAR 2006},
  year = {2006},
  editor = {Furbach, Ulrich and Shankar, Natarajan},
  number = {4130},
  series = {LNAI},
  pages = {145-150},
  publisher = {Springer-Verlag}
}

@INPROCEEDINGS{Janicic06b,
  author = {Jani{\v c}i{\' c}, Predrag and Quaresma, Pedro},
  title = {Automatic Verification of Regular Constructions in Dynamic Geometry
	Systems},
  booktitle = {Proceedings of the ADG06},
  year = {2006}
}

@article{Matsuda04,
	author = {Matsuda, Noboru and Vanlehn, Kurt},
	title = {Gramy: A Geometry Theorem Prover Capable of Construction},
	journal = {Journal of Automated Reasoning},
	year = {2004},
	number = {32},
	pages = {3-33},

}

@inproceedings{Narboux04,
   author    = {Narboux, Julien},
   title     = {A Decision Procedure for Geometry in Coq},
   booktitle = {Proceedings TPHOLS 2004},
   year      = {2004},
   publisher = {Springer},
   volume    = {3223},
   series    = {Lecture Notes in Computer Science}
}

@Article{narboux2006b,
  author =       {Julien Narboux},
  title =        {A Graphical User Interface for Formal Proofs in Geometry},
  year =         {2006},
  editor =       {David Aspinall and Christoph Lüth},
  journal =         {the Journal of Automated Reasoning special issue on User In
terface for Theorem Proving},
  note =         {to appear},
  url =          {\url{http://www.lix.polytechnique.fr/Labo/Julien.Narboux/paper
s/JARuitp-narboux.ps.gz}},
}

@InProceedings{Narboux2006c,
  author =       {Julien Narboux},
  title =        {Mechanical Theorem Proving in {T}arski's geometry},
  booktitle =    {Proceedings of Automatic Deduction in Geometry 06},
  year =         {2006}
}

@TECHREPORT{Nevins74,
  author = {Nevins, Arthur J.},
  title = {Plane Geometry Theorem Proving Using Forward Chaining},
  institution = {MIT},
  year = {1974},
  type = {AI Lab memo},
  number = {303},
  month = {Jan},
  abstract = {A computer program is described which operates on a subset of plane
	geometry. Its performance not only compares favorably with previous
	computer programs, but within its limited problem domain (e.g. no
	curved lines nor introduction of new points), it also invites comparison
	with the best human theorem provers. The program employs a combination
	of forward and backward chaining with the forward component playing
	the more important role. This, together with a deeper use of diagrammatic
	information, allows the program to dispense with the diagram filter
	in contrast with its central role in previous programs. An important
	aspect of human problem solving may be the ability to structure a
	problem space so that forward chaining techniques can be used effectively.}
}

@TECHREPORT{Quaresma06b,
  author = {Quaresma, Pedro and Janicic, Predrag},
  title = {Framework for Constructive Geometry (Based on the Area Method)},
  institution = {Centre for Informatics and Systems of the University of Coimbra},
  year = {2006},
  number = {2006/001}
}

@TECHREPORT{Quaresma06c,
  author = {Quaresma, Pedro and Janicic, Predrag},
  title = {GeoThms - Geometry Framework},
  institution = {Centre for Informatics and Systems of the University of Coimbra},
  year = {2006},
  number = {2006/002}
}

@ARTICLE{Quaresma06d,
  author = {Quaresma, Pedro and Jani{\v c}i{\'c}, Predrag},
  title = {Integrating Dynamic Geometry Software, Deduction Systems, and Theorem
	Repositories},
  journal = {Lecture Notes in Artificial Inteligence},
  year = {2006},
  volume = {4108},
  pages = {280-294},
  number = {4108},
  address = {Heildelberg},
  booktitle = {MKM 2006},
  editor = {Borwein, J. and Farmer, W.},
  publisher = {Springer-Verlag},
  series = {LNAI}
}

@Book{Tarski51,
  author =       {Alfred Tarski},
  title =        {A decision method for elementary algebra and geometry},
  year =         {1951},
  publisher =    {University of California Press}
}

@InProceedings{Tarski59,
  author =       {Alfred Tarski},
  title =        {What is Elementary Geometry?},
  booktitle =    {The axiomatic Method, with special reference to Geometry and P
hysics},
  editor =       {L. Henkin, P. Suppes and A. Tarski},
  publisher =    {North-Holland},
  year =         {1959},
  address =      {Amsterdam},
  pages =        {16--29}
}

@misc{wikipediaDesarguesTheorem,
   title     = {Desargues' theorem},
   year      = {2006.},
   howpublished = {From Wikipedia, the free encyclopedia},
   note      = {http://en.wikipedia.org/wiki/Desargues%27_theorem}
}

@InCollection{Wu78,
  author =       {Wen-Tsün Wu},
  title =        {On the decision problem and the mechanization of theorem proving in elementary geometry},
  booktitle =    {Scientia Sinica},
  volume =       {21},
  pages =        {157--179},
  year =         {1978}
}

@article{Zhang95,
   author    = {Zhang, Jing-Zhong and Chou, Shang-Ching and Gao, Xiao-Shan},
   title     = {Automated production of traditional proofs for theorems in Euclidean geometry
       I. The Hilbert intersection point theorems},
   journal   = {Annals of Mathematics and Artificial Intelligenze},
   pages     = {109-137},
   year      = {1995},
   volume    = {13}
}

