%0 Journal Article %1 keyhere %A Quaresma, Pedro %A Janičić, Predrag %D 2006 %J Mathematical Knowledge Management %K dynamic geometry proving pt theorem %P 280--294 %T Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories %U http://dx.doi.org/10.1007/11812289_22 %X The axiomatic presentation of geometry fills the gap between formal logic and our spatial intuition. The study of geometry is, and will always be, very important for a mathematical practitioner. GCLCprover, an automatic theorem prover (ATP) integratedwith dynamic geometry software (DGS) gives its user a tool to bridge his/her spatial intuition with formal, Euclidean geometryproofs. GeoThms, a system consisting of the mentioned programs and a database geoDB, provides a framework for exploring geometricalknowledge. A GeoThms user can browse through a list of available geometric problems, their statements, illustrations, andproofs. He/she can also interactively produce new geometrical constructions, theorems, and proofs and add new results to theexisting ones. GeoThms framework provides an environment suitable for new ways of studying and teaching geometry at differentlevels. GeoThms also provides a system for storing mathematical knowledge (in a explicit, declarative form) — not only theoremstatements, but also their (automatically generated) proofs and corresponding illustrations.

@article{keyhere, abstract = {The axiomatic presentation of geometry fills the gap between formal logic and our spatial intuition. The study of geometry is, and will always be, very important for a mathematical practitioner. GCLCprover, an automatic theorem prover (ATP) integratedwith dynamic geometry software (DGS) gives its user a tool to bridge his/her spatial intuition with formal, Euclidean geometryproofs. GeoThms, a system consisting of the mentioned programs and a database geoDB, provides a framework for exploring geometricalknowledge. A GeoThms user can browse through a list of available geometric problems, their statements, illustrations, andproofs. He/she can also interactively produce new geometrical constructions, theorems, and proofs and add new results to theexisting ones. GeoThms framework provides an environment suitable for new ways of studying and teaching geometry at differentlevels. GeoThms also provides a system for storing mathematical knowledge (in a explicit, declarative form) — not only theoremstatements, but also their (automatically generated) proofs and corresponding illustrations.}, added-at = {2008-05-22T13:53:16.000+0200}, author = {Quaresma, Pedro and Janičić, Predrag}, biburl = {https://www.bibsonomy.org/bibtex/2a358671b098d0b982c948a8f73a590fe/toni}, description = {SpringerLink - Book Chapter}, interhash = {3323a8d6733f4583154d195b45b92608}, intrahash = {a358671b098d0b982c948a8f73a590fe}, journal = {Mathematical Knowledge Management}, keywords = {dynamic geometry proving pt theorem}, pages = {280--294}, timestamp = {2008-06-05T14:36:10.000+0200}, title = {Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories}, url = {http://dx.doi.org/10.1007/11812289_22}, year = 2006 }