Automated Deduction and Knowledge Management in Geometry
- PDF / 1,827,381 Bytes
- 20 Pages / 547.087 x 737.008 pts Page_size
- 3 Downloads / 194 Views
Mathematics in Computer Science
Automated Deduction and Knowledge Management in Geometry Pedro Quaresma
Received: 12 April 2020 / Accepted: 26 April 2020 © Springer Nature Switzerland AG 2020
Abstract Scientific research and education at all levels are concerned primarily with the discovery, verification, communication, and application of scientific knowledge. Learning, reusing, inventing, and archiving are the four essential aspects of knowledge accumulation in mankind’s civilisation process. In this cycle of knowledge accumulation, which has been supported for thousands of years by written books and other physical means, rigorous reasoning has always played an essential role. Nowadays this process is becoming more and more effective due to the availability of new paradigms based on computer applications. Geometric reasoning with such computer applications is one of the most attractive challenges for future accumulation and dissemination of knowledge. Keywords Automated deduction in geometry · Knowledge management in geometry · Dynamic geometry Mathematics Subject Classification Primary 68T15; Secondary 68P20
1 Introduction “Logic appears in a sacred and in a profane form. The sacred form is dominant in proof theory, the profane form in model theory” D. van Dalen, Logic and Structure [74]. With the ever-increasing power of modern computing and communication devices on symbolic and numeric calculation, the dynamic geometry systems (DGS) and computer algebra systems (CAS) are now mature tools. Using these systems, one can explore geometric figures, experience what happens when dragging part of a figure, perform geometric computation, diagram (or function graph) drawing, knowledge discovering, and create vivid course-ware. Because of the interactive features and powerful problemsolving functions, these systems, stand-alone or integrated in platforms, e.g. in learning platforms like Tabulae [51], GeoThink [52], and Web Geometry Laboratory [62], begins to be widely used in technology-enhanced applications of geometry. This work is funded by national funds through the FCT-Foundation for Science and Technology, I.P., within the scope of the project CISUC-UID/CEC/00326/2020 and by European Social Fund, through the Regional Operational Program Centro 2020. P. Quaresma (B) CISUC, Department of Mathematics, University of Coimbra, Coimbra, Portugal e-mail: [email protected]
P. Quaresma
The integration of geometry automated theorem provers (GATP) in DGS was already done in systems like GCLC [37], GeoGebra [2], GeoProof [54] and JGEX [81]. The integration in computer-supported collaborative learning systems or intelligent tutoring systems is beginning to became a reality, e.g. QED-Tutrix [27,45]. The integration of GATP in other tools raises many questions that transcend the GATP themselves, going into the area of knowledge management. To be able to build systems capable of harnessing in its fullest the GATP capabilities, we need: an open source library of GATP [57]; application programming interfaces (APIs) and common for
Data Loading...
