![]() |
Proof Interpretation |
![]() |
AProVE Help System → Proof Output → | Proof Interpretation |
AProVE is able to generate proof outputs in HTML, LaTeX and plain text format. For more information how to generate and save the different formats, please click here.
We will explain the layout of a typical proof using the HTML output.
The layout in LaTeX or plain text is very similar; LaTeX additionally offers
images of graph structures instead of a text based representation.
Every proof layout consists of three characteristic elements:
The header consists of basic information about the obligation which has to be shown (for example termination or liveness). For example, it looks like this:
Term Rewriting System R:
[y, x]
le(0,
y)
-> true
le(s(x),
0)
-> false
le(s(x),
s(y))
-> le(x,
y)
minus(0,
y)
-> 0
minus(s(x),
y)
-> ifminus(le(s(x),
y),
s(x),
y)
ifminus(true,
s(x),
y)
-> 0
ifminus(false,
s(x),
y)
-> s(minus(x,
y))
mod(0,
y)
-> 0
mod(s(x),
0)
-> 0
mod(s(x),
s(y))
-> ifmod(le(y,
x),
s(x),
s(y))
ifmod(true,
s(x),
s(y))
-> mod(minus(x,
y),
s(y))
ifmod(false,
s(x),
s(y))
-> s(x)
Termination of R to be shown.
In the proof body, the work of AProVE's actual techniques is shown. Every technique which was used for the proof is mentioned in the following way:
Locator: A tree structure indicates where this technique appeares in the proof. In the example above, the Dependency Pair Analysis has the following locator:
R ↳ NOC → TRS2 ↳Dependency Pair Analysis |
This structure is similar to a part of the proof tree shown in the Result Viewer .It means that the Dependency Pair technique was used after a Non-Overlappingniss Check (NOC) was used on the original Term Rewriting System R, leading to a new Term Rewriting System TRS2. This system is source for the current Dependency Pair Analysis.
Current Obligation: After the locator, in some cases follows the current obligation which has to be proved, e.g. a Term Rewrite System or a Strongly Connected Compounend (SCC). A SCC is presented graphically in the LaTeX output. Because the Non-Overlappingness Check in the example above did not change anything essentiell in the Term Rewriting System, the current obligation is not mentioned here.
Proof Technique Summary: This is the main information of the technique used on the current obligation. Please look at the summary of all techniques currently used in AProVE to understand what happens here. In our example, the Dependency Pair Analysis has generated the following summary:
R contains the following Dependency
Pairs:
Furthermore, R contains three SCCs. |
So AProVE has detected the Dependency Pairs above and three SCCs. These SCCs are new obligations, whose termination has still to be shown. This is reflected in the next locator, which illustrates the work of the next technique applied to the new obligations. In our example, the Size-Change Principle is applied to the first of the three SCCs:
R ↳NOC → TRS2 ↳DPs → SCC1 ↳Size-Change Principle → SCC2 ↳SCP → SCC3 ↳Polo |
Thus the structure in the Proof's body repeats.Longer paths from the tree's root to a leaf are shortened in the full proof view (not in the Result Viewer ).
The conclusion at the proof's end summarizes the success of the whole proof.
Termination
of R successfully shown.
Duration: 0:05 minutes |
As You can see in the document structure description above, colours in the locator (and the same way in the Result Viewer ) represent the success status of AProVE's techniques. There are three important colors in Results:
Consider the following example:
On the path to the Non-Termination check there was a tranformation (Context Sensitive to Term Rewriting System) which did not preserve the completeness of Non-Termination. So the local result Non-Termination cannot state anything. Therefore it is propagated upwards as a failure in yellow. And indeed the original System terminates, so it would not be a good idea to show Non-Termination. In other cases, locally prooved Termination does not suffice for global success, because it was only successful for one of many obligations, of which others could not be evidenced to be terminating.