Skip to content
This repository

Speedith is a theorem prover for spider diagrams (see http://en.wikipedia.org/wiki/Spider_diagram).

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 Speedith.Core
Octocat-spinner-32 Speedith.Gui
Octocat-spinner-32 devel
Octocat-spinner-32 docs
Octocat-spinner-32 .gitignore
Octocat-spinner-32 README.md
Octocat-spinner-32 pom.xml
README.md

Speedith


Speedith is a diagrammatic theorem prover for spider diagrams.


Developer's Guide to Speedith


General Requirements

These requirements have to be checked only once. After you make sure you have these, you can build Speedith at any time.

  • iCircles sources: You can get the sources of iCircles from GitHub.

    You may simply want to execute this in the command line:

        git clone https://github.com/urbas/iCircles.git
        cd iCircles
        mvn install
    
  • Propity Library: You can get the sources from GitHub.

    Execute this in the command line:

        git clone https://github.com/urbas/mixr.git
        cd mixr/Propity
        mvn install
    

Building Speedith

Use Maven to build Speedith (in the root directory of your cloned Speedith repository):

mvn install

Running Speedith

After a successful build, you can run Speedith by firstly entering the Speedith.Gui directory:

cd Speedith.Gui

and then running:

mvn exec:java -Dexec.mainClass=speedith.Main

Using Speedith in Isabelle/HOL

MixR (the name of the Speedith/Isabelle integration) requires some special settings for Isabelle. You can find sample settings in the Speedith distribution's 'settings' file.

You can either edit your existing Isabelle settings, or copy the included 'devel/Theories/settings' file to Isabelle's user settings folder (e.g. '~/.isabelle/Isabelle2011-1/etc/').

Something went wrong with that request. Please try again.