Saturation Visualization for Vampire

This tool visualizes Saturation Runs of Vampire, with the main aim to let a user quickly answer the following questions:

Which consequences are derived?
- Which of the consequences we anticipated were derived?
- Which other interesting consequences were derived?
- Which proof was found by Vampire?
Why didn’t we derive a certain clause?
- Forgot to add some trivial fact to the encoding
- Ordering doesn’t allow inference
- Weight is to big for clause to be selected
- ...

There are three modes:

Proof: Run Vampire on the problem. If a proof is found, visualize it.
Saturation: Run Vampire on the problem. Visualize the whole saturation attempt.
Manual Clause Selection: Run Vampire on the problem, but interactively decide in each step which clause Vampire should explore next.

Running the visualization

Step 1: Install and run a Vampire Server

Described at https://github.com/gleiss/server-vampire

The Vampire Server is used as backend by the Saturation Visualization.

Step 2: Access the Saturation Visualization

https://gleiss.github.io/saturation-visualization/

The Saturation Visualization communicates with the Vampire Server on localhost:5000.