This is your login information: Your username is: beeson If you forgot your password, you can click the 'Send Login Details' link on the EM Login page at https://amai.editorialmanager.com/. When revising your work, please submit a list of changes or a rebuttal against each point which is being raised when you submit the revised manuscript. Your revision is due by 25 May 2018. To submit a revision, go to the above URL and log in as an Author. You will see a menu item called 'Submissions Needing Revision'. You will find your submission record there. Please make sure to submit your editable source files (i. e. Word, TeX) Yours sincerely Maria Verna Remellite JEO Assistant Annals of Mathematics and Artificial Intelligence Reviewers' comments: Reviewer #2: This paper presents a mechanized version of Euclid's Book I. A dedicated proof system for a weak version of first-order logic has been developed for checking the proofs. Translations to the proof assistants HOL-Light and Coq have been written in order to recheck all the proofs and derive further properties of the axiomatic system that is used in this mechanization. The article is quite enjoyable to read. Getting a formal version of Euclid Book is clearly an interesting contribution of the paper. The presentation could be slightly improved. Here are some suggestions. 1) It is not clear to me why Coq or HOL-Light could not have been used to design the axiomatic. The need for an extra proof checker should be more clearly motivated. [This point has been addressed middle of p. 22 ] 2) I find that the somewhat vintage choice of a string-based syntax makes it really difficult for a human being to read the actual formal code. A translator to Latex would be nice to get a more human-readable version of the appendix. It would also make the contribution of the paper more accessible. [We want to use a format that can be cut and pasted, even from a pdf file. Thus LaTeX is not suitable. The referee also requested an example of one of our formal proofs, which will necessarily be in Polish notation. We could put the axioms and definitions either in Polish or in HOL Light notation in verbatim mode. ] 3) In the paper there are lot of discussion about the quality of the axiomatic system but very few about the acutal proofs. I think it would be nice to have at least of example of a comparison between a textual proof and a formal proof. [Appendix 1 has been added, with the formal proof of Prop. I.1. The reader may compare it to Euclid's text.] 4) This is somewhat related to 3). It is not clear to me what is the level of granularity at which the formal proof can be given. What is the level of automation that is needed in order to check the proof. The only figures I could find are the one given for the checking time for the translation in HOL and Coq. More than 1/2 hour for checking 100 proofs seem a lot to me. [Our custom proof checker takes only seconds to check all the proofs. ] Other Remarks Page 14 Line 12 : footnote 17 has no association [ There was an accidental extra space near that footnote--fixed.] Page 14 Line 18 : I guess there is something missing AB = DB and CA = CD? [Yes, fixed.] Page 16 Line 31 : "are" -> "and" [Fixed] Page 19 Line 12 : "a form that would be easy to manipulate by computer" this is debatable. Books like "Handbook of Practical Logic and Automated Reasoning" show that there are interesting alternative to string. [Maybe so, but it certainly isn't debatable that strings are easy to manipulate.] Page 19 Line 51 : "postulate,proposition" -> ", proposition" [missing space fixed] Page 20 Line 13 : "arguments by contradiction" does this mean that it assumes classical logic. [Yes, in a sense, although "classical" logic didn't existe until millenia after Euclid, and Euclid didn't use quantifiers. Our system Euc follows Euclid, not classical logic.] Page 22 Line 44 : "In essence we have proved that the axioms hold in any model." Any model of what? I am not sure I understand the point of this whole paragraph [clarified the text] Page 24 Line 15 "F_" why some variables have underscore? [In order to avoid conflict with predefined F. This isn't worth mentioning.] Page 25 Line 37-38 : "Whether the proofs are correct with respect to the 'natural' interpretation of the proof steps (whatever that is) is not checked in the HOL version." I am not sure what you mean by this. You check that the conclusion is a consequence of the assumptions but you are not sure that the justification is relevant? [Freek, please clarify in freek.tex] Page 28 Line 23-24 : "45 minutes" would it possible to have a more detailed account. How much time is taken by searching the proofs and how much time on checking them. Page 29 Line 35 : "the predicate CI" which predicate CI? [The one which is (now) introduced on page 6] Page 29 Line 37 : "J = (C, A, D)" is this Leibniz equality? [Yes] Page 29 Line 51 : "the the" only one [fixed] Page 29 Line 51 : "hole" -> hold [fixed] Page 30 Line 9 : "times" -> \times [changed] Page 30 Line 32-33 : "squares of their signed areas" why not simply using the absolute as it is used later Page 30 Line 42 : "footnote 24" it would be nice to have an update of this effort. [We finished this verification as promised and reported on it in a new section.] Reviewer #3: As ever with such formalisations of Euclid, the relation between the original text and the formalisation is strained. When formalising one necessarily interprets and those interpretations pull against the accuracy of the formalisation to the text. Yet this formalisation is quite interesting and is worth publication despite its historical inaccuracies. The main inaccuracy I want to mention is the use of betweenness axioms. Hilbert following Pasch added these but that is because both wanted to avoid diagrammatic reasoning. In Euclid however betweenness suppositions are tacit in the use of diagrams. [ Yes, they are tacit, but that leads to errors, as has been pointed out as long ago as Proclus. The "tacit" introduction of unjustified conclusions leads to flaws and outright errors. Witness the example we gave concerning the bisector of an angle: why does the line lie in the interior of the angle? The "tacit" assumption (for it cannot be labeled anything more than "assumption") that it does lie in the interior is just erroneous reasoning. This is exactly the kind of flaw that Hilbert and Pasch wanted to correct, and we, following Hilbert and Pasch but with computer-supported tools, can actually do.] This diagram use is not linguistic and so is not expressed in axioms, yet it is rigourous nonetheless. [This point has been addressed in the new paragraphs added at the end of the paper, before the Appendices.] So a historically accurate formalisation would include the diagrammatic inferences as primitive inferences, not in need of axiomatic reformulation. See Manders for more on this. Despite this the paper should be published because the theorems obtained by Euclid are expressed linguistically, and so one can seek other, not historically Euclidean, means to proof them. This paper analyses a logically plausible formalisation that shows the provability of Euclid's book I theorems. In that it is in the spirit of the reconstructionists Hilbert and Tarski, adding here modern formal proof checkers.