@article{keyhere,
	title = {Automatic Verification of Regular Constructions in Dynamic Geometry Systems},
	author = {Predrag Janičić and Pedro Quaresma},
	journal = {Automated Deduction in Geometry},
	pages = {39--51},
	url = {http://dx.doi.org/10.1007/978-3-540-77356-6_3},
	year = {2007},
	biburl = {http://www.bibsonomy.org/bibtex/2ef89f20bb3022487552c7ca62d17a296/toni},
	description = {SpringerLink - Book Chapter},
	abstract = {We present an application of automatic theorem proving (ATP) in the verification of constructions made with dynamic geometry
software (DGS). Given a specification language for geometric constructions, we can use its processor to deal with syntacticerrors. The processor can also detect semantic errors — situations when, for a given concrete set of geometrical objects,a construction is not possible. However, dynamic geometry tools do not test if, for a given set of geometrical objects, aconstruction is geometrically sound, i.e., if it is possible in a general case. Using ATP, we can do this last step by verifyingthe geometric constructions deductively. We have developed a system for the automatic verification of regular constructions(made within DGSs GCLC and Eukleides), using our ATP system, GCLCprover. This gives a real-world application of ATP in dynamicgeometry tools.},
	keywords = {dynamic geometry proving theorem }
}