Commit 2618ec06 authored by Dennis Müller's avatar Dennis Müller

update

parent 4c0a8b62
......@@ -8,7 +8,7 @@ Regarding the specifically sugessted libraries: The algorithm in general require
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. 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.
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.
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.
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").
......
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