Prooftree opens one window for each proof that it is requested to display. This window contains the
proof-tree graph and a small display for sequents and proof commands.
Colors
The branches in the proof-tree graph are colored according to their state. Prooftree distinguishes
between the following states.
current (blue by default)
The current branch is the branch from the root of the proof tree to the current goal.
unproven (default foreground color)
A branch is unproven if it contains open proof goals.
proved incomplete (cyan by default)
An incompletely proved branch has its proof finished, but some of the existential variables that
have been introduced in this branch are not (yet) instantiated.
proved partially (dark green by default)
In a partially proved branch all existential variables of the branch itself are instantiated, but
some of those instantiations contain existential variables that are not (yet) instantiated.
proved complete (green by default)
A branch is proved complete if all its existential variables are instantiated with terms that
themselves do not contain any existential variables.
cheated (red by default)
A cheated branch contains a cheating proof command, such as admit
The colors as well as many other Prooftree parameters can be changed in the ProoftreeConfigurationDialog (see below).
Navigation
When the proof tree grows large one can navigate by a variety of means. In addition to scroll bars and
the usual keys one can move the proof tree by dragging with mouse button 1 pressed. By default, dragging
moves the viewport (i.e., the proof tree underneath moves in the opposite direction). After setting a
negative value for Dragacceleration in the ProoftreeConfigurationDialog, dragging will move the proof
tree instead (i.e, the proof tree moves in the same direction as the mouse).
SequentDisplay
The sequent display below the proof tree normally shows the ancestor sequent of the current goal. With a
single left mouse click one can display any goal or proof command in the sequent display. A single click
outside the proof tree will switch back to default behavior. The initial size of the sequent display can
be set in the ProoftreeConfigurationDialog. A value of 0 hides the sequent display.
ToolTips
Abbreviated proof commands and sequents are shown in full as tool tips when the mouse pointer rests over
them. Both, the tool tips for abbreviated proof commands and for sequents can be independently switched
off in the ProoftreeConfigurationDialog. The length at which proof commands are abbreviated can be
configured as well.
AdditionalDisplays
A double click or a shift-click displays any goal or proof command in an additional window. These
additional windows are automatically updated, for instance, if an existential variable is instantiated.
For additional sequent displays one can browse the instantiation history of the sequent using the forward
and backward buttons. These additional windows can be detached from the proof tree. A detached display is
neither automatically updated nor automatically deleted.
ExistentialVariablesProoftree keeps track of existential variables, whether they have been instantiated and whether they
depend on some other, not (yet) instantiated existential. It uses different colors for proved branches
that contain non-instantiated existential variables and branches that only depend on some not
instantiated existential. The list of currently not (yet) instantiated existential variables is appended
to proof commands and sequents in tool-tips and the other displays.
The ExistentialVariableDialog displays a table with all existential variables of the current proof and
their dependencies. Each line of the table contains a button that marks the proof command that introduced
this variable (with yellow background, by default) and, if present, the proof command that instantiated
this variable (with orange background, by default).
MainMenu
The Menu button displays the main menu. The Clone item clones the current proof tree in an additional
window. This additional window continues to display a snapshot of the cloned proof tree, no matter what
happens with the original proof.
The Showcurrent and Showselected items move the viewport of the proof tree such that the current proof
goal, or, respectively, the selected node will be visible (if they exist).
The Exit item terminates Prooftree and closes all proof-tree displays.
The remaining three items display, respectively, the ProoftreeConfigurationDialog, and the Help and
About windows.
ContextMenu
A right click displays the ContextMenu, which contains additional items.
The item Undotopoint is active over sequent nodes in the proof tree. There, it sends an retract or undo
request to Proof General that retracts the scripting buffer up to that sequent.
The items Insertcommand and Insertsubproof are active over proof commands. They sent, respectively, the
selected proof command or all proof commands in the selected subtree, to Proof General, which inserts
them at point.
Install Now
SVG Icons
