Commit 42bf93cd authored by Dennis Müller's avatar Dennis Müller

update

parent 2618ec06
......@@ -15,7 +15,7 @@ Reviewer #4 asked about why we were looking for views *out of* our example theor
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.
The instatiation of theory parameters in our discussion of their contravariant elimination would indeed not be possible during the viewfinding process itself and would be part of the preprocessing of theories.
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.
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.
......
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