Open AccessChallenge to the proving of theorems of Euclid's elements of as ATP
Publication year - 2019
Publication title -
journal of engineering and science research
Language(s) - English
Resource type - Journals
ISSN - 2289-7127
DOI - 10.26666/rmp.jesr.2019.4.3
Subject(s) - hol , automated theorem proving , euclidean geometry , proof assistant , point (geometry) , mathematics , calculus (dental) , computer science , discrete mathematics , algebra over a field , mathematical proof , programming language , pure mathematics , geometry , medicine , dentistry
Automated theorem proving (ATP) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. An Isabelle/HOL is a generic proof assistant. We perform the challenge for the proving theorems of Euclid's elements of geometry. We could prove some theorems of Euclid's elements of geometry. Technique of programing and mental conception interact. The mathematics education which prove theorems of the Euclidean geometry by using the Isabelle/HOL can correct the present weak point