Commit 0b3a3ddf authored by Florian Rabe's avatar Florian Rabe
Browse files

no message

parent 42bf93cd
First, we would like to thank the reviewers for their positive and constructive feedback.
We thank the reviewers for their constructive feedback.
We will take care of all minor comments.
Regarding the major comments:
Review 1:
The main bottleneck is indeed the cost of representing mathematical libraries faithfully.
But those decrease as we gain experience and community interest grows, and we now have representations of PVS, HOL Light, Mizar, and IMPS.
For informal libraries like Mathematical Structures, a parsing effort is needed the cost of which can vary a lot.
For example, for OEIS, it took a student several months.
Review 2:
We will prepare an extended version with algorithm details, proofs, and run time analyses to be available online.
Review 3:
The need for some familiarity with MMT and/or NASA is unfortunately inherent in the topic.
But when going over the paper again, we'll try to make it more accessible.
The extended online version will also help here.
Review 4:
Knowledge in Isabelle/HOL, Coq, and Mizar can be accessed analogously to PVS.
However, the theory structure there is often implicit, and it is still an open question which heuristic for introducing theory structure will work best.
We will try to add more details to Sect. 4.2, at least in the extended version.
FR: Old version below the line; should not be submitted.
As a general comment, we should mention that an earlier draft of this paper covered some of the criticism presented, but this had to be shortened severely due to the page limitations. In as far as we are not able to cover all of the clarifications requested, we will consider publishing an extended version of the paper online.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment