You will find a zip file containing the 2016 version of Speedith at the following link:


Extract the archive. This will create the Speedith executable, speedith.jar and a folder with examples.


Please follow these instructions:

To use Speedith with Euler diagrams, please open the Preferences
(File->Preferences) on the first Startup.

  1. Tab Diagram Type: Choose Euler Diagrams
  2. Tab Tactics: Check Show low level-tactics if you want to see/apply all
    possible tactics provided by Speedith. Otherwise, only the high-level
    tactics (Venn (Depth), Venn (Breadth) and Copy Shading and Contours) will
    be available.
  3. Tab Auto Prover: Check that the automatic proof search in the background
    is switched of. The implementation of the automatic prover is only a prototype and tends to use up all memory that is available.


Examples of both proofs and proof goals are contained in the examples folder. The subfolder paper contains all proofs and proof goals mentioned in the submission to UITP 2016.


Requirements: Java 7

(Speedith has not been tested with Java 8. It might work or it might not.)


This version of Speedith has been compiled and tested on Ubuntu 16.04 (LTS). It should work on MacOS and Windows as long as a Java Runtime Environment is present, but we cannot give any guarantees.