Jambox | Automated Termination Proofs For String and Term Rewriting

What is Jambox?

Jambox is an automated termination prover for string and term rewriting systems.
The main new techniques are:
used in conjunction with Dependency Pairs Transformation, Subterm Criterion, Self-Labeling, Semantic Labeling and Reducing Right-Hand Sides, see Jambox Theorems/References 2006 for a complete list of references.

Special thanks go to:
  • SatELite/MiniSat a cutting-edge SAT solver. Jambox depends to a great part on the strength of SatELite for finding Matrix Interpretations.
trivia: The name Jambox is an abbreviation for JavaMatchbox, which has been adopted from Matchbox, the first termination prover using match bounds.

3rd Party Libraries

Jambox uses the following 3rd Party Libraries:
  • SatELite/ MiniSat a cutting-edge SAT solver.
    (heavily used by Jambox to find suitable matrix interpretations)
  • GLPK (GNU Linear Programming Kit)
    (used to find 1x1 matrix interpretations)
  • dk.brics.automaton a automaton/regexp package for Java.
    (used to transform regular expressions into finite state automata)
  • Retroweaver a bytecode weaver for Java.
    (allows us to develop against Java 1.5 and deploy on 1.4)
  • TouchGraph a library for graph visualization.
    (used to view the life construction of compatible automata)

Download binaries

In order to start Jambox you will need to get Java 1.5 installed on your system. You can download Java 1.5 from Sun Microsystems.

By downloading Jambox argree to the license of the included 3rd party tools:
Download the precompiled binaries:
Jambox 2.0e (WST competition version 2006)

Install Jambox:
Extract the jambox2e.tar.gz to the desired installation location. Edit the INSTALLDIR variable within the jambox/runme shell-script to point to the jambox installation directory. Finally run the Jambox-selftest to verify that the installation was successful and Jambox is able to find its required external libraries. 
$./runme test
Checking for dk.brics.automaton... ok
Checking for GLPK... ok
Checking for timeout... ok
Checking for SatEliteGTI... ok
Start Jambox:
$./runme file.srs/trs

Build from Sources

Sources will be availiable soon.

Usage of Jambox

Currently there is only a command-line version of Jambox available. Jambox generates a .html file as output (might be more than 100kB in size). Therefore the preferred way to use Jambox is to redirect the generated proof into a file and to view this file using a web browser. 
$./runme file.srs/trs > output.html
firefox output.html
where "file.srs" is the name of a file containing the SRS rules (comma separated): 
(RULES a a -> a b a , b a b -> a c a)
resp. "file.trs" is the name of a file containing the TRS rules (without comma): 
(VAR x y)
(RULES f(f(x,a),y) -> f(y,f(x,y)))

Useful information

Theoretical background is presented in papers by: Other automated termination provers that use Matrix Interpretations and/or Match-bounds:
  • Matchbox Rewriting with Height Annotations for SRS and TRS
  • AProVE Lehr- und Foschungsgruppe Informatik II, RWTH Aachen
  • TORPA by Hans Zantema, TU Eindhoven
  • TTTBox by Martin Korp
Jambox took part in the SRS/TRS category of the Termination Competition in 2005 and 2006.