Proof Exploration

-- Author: Alexander Weigl, August 2021 valid for KeY-2.10.0

Abstract

This note describes the Proof Exploration features in KeY-2.10. Proof Exploration allows a flexible editing of sequences, and therefore brings a "What-If"-Analyses into KeY.

Overview

We aggregrate under Proof Exploration, actions and views for supporting a What-If analysis. With the here described actions you can investigate the proof state and try to figure why a proof does not close.

For this we offer following actions:

Proof Nodes, which are affected of exploration actions, are marked in the Proof Tree.

Attention

Proof Exploration actions are only available if you activate the Exploration Mode in the toolbar.

Actions

Views

Image of Exploration Steps

Visualization of performed exploration actions. To jump to a node where the action was applied to select the entry in the list or the tree view. To prune exploration actions simply select an action and all action below this action (visible in the tree visualization) are removed.