MixR is a heterogeneous reasoning framework. It is based on the NetBeans Plathfom and highly extensible. Via MixR drivers existing theorem provers are extended with HR.
Java Scala Isabelle Other
Switch branches/tags
Nothing to show
Latest commit d0802f4 Oct 5, 2014 @urbas Fixed references to propity.
Permalink
Failed to load latest commit information.
devel
external/libs More fixing after renaming. Jan 19, 2013
graphics - Committed the remainder after the rename. May 2, 2012
libs Added more test formulae into the theory file. Jan 8, 2014
.gitignore Removed a lot of nulls from the primary spider diagram. Nov 4, 2013
LICENSE - Added some README content and the licence. Apr 23, 2012
README.md
pom.xml Fixed references to propity. Oct 5, 2014

README.md

MixR

MixR is a framework for integrating multiple sentential and diagrammatic theorem provers, as well as informal tools from arbitrary domains (such as image processing, natural language processing, amongst others) into one heterogeneous reasoning system.

MixR is a conglomeration of modules built for the NetBeans Platform. It integrates well with I3P (an interactive interface for the Isabelle prover).

This project is related to (but not dependent on) Speedith (a diagrammatic theorem prover for spider diagrams).

Speedith and Isabelle (through I3P) are the first supported theorem provers to be integrated into the MixR framework--resulting in the Diabelli Heterogeneous Reasoning System. With Diabelli it is possible to use spider diagrams while performing proofs in Isabelle. Isabelle formulae are automatically translated to spider diagrams if possible. The user can then reason on the spider diagram and then return the result of reasoning with the spider-diagrammatic representation back to Isabelle.

We provide two further examples of heterogeneous reasoning with MixR:

  1. NatLang: demonstrates how reasoning with natural languages can be performed in a general-purpose sentential and formal theorem prover (in this case, Isabelle).
  2. PicProc: demonstrates how one can reason about bitmap images within Isabelle.

Both of the examples above use the novel concept of placeholders to insert natural language sentences and images into Isabelle's formulae.

Installation procedure

  1. Download the NetBeans IDE with Java SE support from this location (currently we support NetBeans 7.3):

    https://netbeans.org/downloads/

  2. Install Maven:

    http://maven.apache.org/download.cgi

  3. Clone this repository repository:

    git clone https://github.com/urbas/mixr.git
    
  4. This is enough just to build the MixR framework (without any plugins!). This means that none of the examples (Isabelle, Speedith, NatLang, PicProc, and TPTP will work).

    To build MixR framework (MixR core), open the devel/MixRFramework project in NetBeans.

    To build Diabelli (with Isabelle, Speedith, NatLang, PicProc, and TPTP support), proceed as follows:

  5. Download and unpack Isabelle 2012 into the ~/bin/Isabelle2012 folder. Isabelle 2012 can be downloaded from:

    http://isabelle.in.tum.de/website-Isabelle2012/index.html

    On Mac Isabelle might need Java 6. You can get it from here: http://www.oracle.com/technetwork/java/javase/archive-139210.html

    or here: http://support.apple.com/kb/dl1573

  6. Clone the Speedith and iCircles repositories (follow their installation instructions from README.md):

    git clone https://github.com/urbas/speedith.git
    git clone https://github.com/urbas/iCircles.git
    

    The Speedith and iCircles folders must be siblings to the mixr folder.

  7. Go to the mixr folder and run the following:

    mvn install

  8. Clone I3P from here (you'll need Mercurial for this):

    hg clone https://urbas@bitbucket.org/urbas/i3p
    
  9. Open the Diabelli project (devel/Diabelli) within NetBeans and make sure all dependencies are resolved. Try to build and run.

    Feel free to contact developers in case the build fails.

Licence

MixR is an open source project. It's sources are freely available under the MIT License.

The full text of the licence is in the following file:

<repository root>/LICENSE