Node Differences

-- Author: Alexander Weigl, 24.07.2019

In the context menu of the Proof Tree, you can the action Diff with parent, which triggers a view for visualising the differences between Proof Nodes.



The view shows the serialNr of selected nodes in the top, and the differences between the antecedents and succedents seperately.

The differences for ante- and succedents are calculated in the same fashion:

  1. We consider the ante- and succedents as a set of formulas, therefor formula order doesn't matter.
  2. Given two formulae sets (left and right side) we calculate between each pair the Levensthein degree.
  3. We greedy match the formulae from the left to right side. Starting with exact matches (zero differences) and ending with completely different pairs.

The view shows each matched pair side by side.

Action and Settings

You can: