rebuttal.txt 4.76 KB
Newer Older
Dennis Müller's avatar
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
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.

Dennis Müller's avatar
update    
Dennis Müller committed
11
We acknowledge the preliminary nature of our work. Reviewer #4s assumption that the results for commutative operators are poor are explained by this use case using the PVS/Prelude library only. PVS/NASA could unfortunately not be used for a screenshot because of the memory limitations of the jEdit IDE used as an editor for MMT theories. 
Dennis Müller's avatar
update    
Dennis Müller committed
12
Explaining our results regarding PVS/NASA 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. 
Dennis Müller's avatar
Dennis Müller committed
13

Dennis Müller's avatar
update    
Dennis Müller committed
14
15
16
17
Reviewer #4 asked about why we were looking for views *out of* our example theory of "beautiful sets" (instead of into). The reason being that in this use case we want to see whether the full theory (or instances thereof) already exists in some library. The section "Enabled Applications" in the Conclusion somewhat covers the directionality of the algorithm, including reuse of results as pointed our by the reviewer (see the application "Folklore-based Conjecturing"). 

Our use of "meta-theories" is actually intended to be morally equivalent to the common usage. We assume Reviewer #4s very understandable confusion stems from a lack of provided background on MMT itself. A meta-theory in MMT indeed lives on a different semantic level from a logical point of view - however, one core feature of the MMT system is that all theories are represented uniformly. In fact, LF too is not hard coded in MMT, but a theory in the same sense as e.g. the foundational theory for PVS or a theory within the PVS/NASA library. Hence the meta-theory relation becomes a relation between "object-level" (from the point of view of the MMT system) theories. We will consider adapting the Preliminaries-section accordingly.

Dennis Müller's avatar
update    
Dennis Müller committed
18
The contravariant elimination of theory parameters would indeed not be possible during the viewfinding process itself and would be part of the preprocessing of theories.
Dennis Müller's avatar
update    
Dennis Müller committed
19
20
21

We mention using theorem proving in the beginning of Section 3, but decide to forego this option for the current paper for efficiency reasons. Searching for proofs would be prohibitively expensive for most applications described, where the results of viewfinding should be available while actively editing/writing theories. This is a conscious design choice regarding the trade-off between speed and accuracy. 

Dennis Müller's avatar
Dennis Müller committed
22
23
24
25
26
-------------

[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, http://kwarc.info/kohlhase/papers/icms16-oeis.pdf