Tutorial: Abbreviate Rule





The interactive transcript could not be loaded.


Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Oct 20, 2013

This video is part of a tutorial series for the Theorem Prover KeYmaera.

In this video we show you how to apply the abbreviate rule. This rule is helpful when your proof uses the same or equivalent expressions in more than one place. If the expression you are abbreviating has a lot of variables, it will simplify the computation done by the quantifier elimination algorithm. Or, if your expression causes branching, you can reduce the number of branches taken by the prover.

Let's look at an example. As humans, we can see that this property holds by transitivity. With the complexity of the formulas and the number of variables therein, quantifier elimination will eventually solve the problem, but it may take a very long time. We can help by showing the transitive structure of the problem through abbreviating equivalent terms to a single variable with the abbreviate rule.

Using abbreviate can allow you to give some high-level hints to KeYmaera to guide the proof in the right direction.


When autoplay is enabled, a suggested video will automatically play next.

Up next

to add this to Watch Later

Add to

Loading playlists...