Commit 01769b00 authored by Dennis Müller's avatar Dennis Müller


parent 960af642
First, we would like to thank the reviewers for their positive and constructive feedback.
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.
We are happy to hear Reviewer #1 is interested in representing additional libraries in MMT. This paper is (as mentioned in the Acknowledgments section) part of the OAF project, the goal of which is to represent as many formal libraries as we are able to. Chiefly, we already have representations of the PVS, Mizar, HOL Light and IMPS libraries. Citations for the first three imports ([1],[2]) are below, the fourth has been submitted (and accepted, with lead author Jonas Betzendahl) for CICM as well. We are always open to adding additional Libraries.
Regarding the specifically sugessted libraries: The algorithm in general requires the domains for viewfinding to be sufficiently formal; our implementation additionally requires a representation in MMT/OMDoc. The (apparent?) informality of the mentioned archive of mathematical structures might be prohibitive, but we will gladly look into it. Regarding OEIS, we already have a more specialized tool for searching, see [3].
We regret having to cut short some of the more thorough explanation. The proofs for the lemmata requested by Reviewer #2 are rather straight-forward and not very illuminating, but we will gladly add them to an extended version. We will furthermore add the run times of the algorithm for the use cases covered in the paper, to back up our efficiency claims.
We acknowledge the preliminary nature of our work and that (as mentioned by Reviewer #4) more views should be found in the described PVS/NASA library. However, explaining our results requires investigating and going into detail on the specific methodologies, practices and idiosyncracies of the PVS system in general and the NASA library development in particular. While we could certainly go into more detail, as Reviewer #3 mentions the paper is already somewhat terse without a certain amount of background knowledge regarding PVS, which is not the central topic. We consider analyzing and describing the results in more detail in an extended version.
[1] M. Iancu, M. Kohlhase, F. Rabe, J. Urban - "The Mizar Mathematical Library in OMDoc: Translation and Applications", Journal of Automated Reasoning 50/2, p.191-202
[2] C. Kaliszyk, F. Rabe - "Towards Knowledge Management for HOL Light", Intelligent Computer Mathematics 2014, p.357-372
[3] E. Luzhnica, M. Kohlhase - "Formula Semantification and Automated Relation Finding in the OEIS", ICMS 2016,
Markdown is supported
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