disclaimer: this is old software, that is not supported anymore.

MUPSter: A Prototype for Top-Down Debugging

We have implemented the MUPSter-system as a prototype for the top-down debugging of incoherent terminologies. The system implements the tableau-based approach described in section 3.1.1 to calculate the MUPS of an unsatisfiable concept, the three methods to calculate diagnoses for the incoherence problem, as well as cores, pinpoints and other debugging facilities. MUPSter is implemented in JAVA, and is based on the WELLINGTON reasoner developed at King's College, London. It supports the standard krss format and the DIG language. A given terminology is parsed and analysed, and iteratively debugged in the following order:

1. Unsatisfiable concepts: a request to RACER is send to return a list of unsatisfiable concepts
2. MUPS: for each unsatisfiable concept, the set of MUPS is calculated, using a specialised labelled tableau.
   1. a minimisation function is calculated from the fully expanded tableau
   2. the minimisation function is minimised with an implementation of a hitting- set algorithm to calculate prime-implicant.
   3. these prime implicants are the MUPS.
3. MIPS: MIPS can easily be calculated from the MUPS of all unsatisfiable concepts.
4. The version we provide also calculates MiniMIPS, which are parts of axioms.
5. Pinpoints and Cores
6. Diagnoses: based on the MIPS (as minimal conflict sets) we can calculate diag noses. In the current version, this is switched off, because it usually takes too much time to calculate diagnoses.

Installation and Test Guide

MUPSteris available as a JAVA jar archive, and can, in principal, be executed platform independent on machines running JAVA 1.5.1. MUPSter performs debugging on incoherent ALC-terminologies. If the terminology is unfoldable, the algorithms calculate the set of all MUPS, MIPS and diagnoses. Otherwise, the algorithm is incomplete, and the results can often be not very useful.

MUPSterstill is an experimental prototype, and in some cases problems will most probably occur. However, installing and running MUPSter is very easy, simply follow the instructions below:

1. Download MUPSter: Download the file mupster.jar from here.
2. Pre-process ontology: MUPSter's parsers are for the time being not very robust, and the language accepted is rather restricted. On the previously mentioned website, some scripts are available for convenience to transform a krss ontology into format where problems could be avoided.
3. Download RACER: MUPSter requires RACER to run as a server as external DL reasoner.
4. Start RACER: The RACER server has to be started and listen to the default port:8000
5. Run MUPSter: Under Linux run MUPSter with the following command line:
   • java -jar mupster.jar -f file.krss (options) for ontologies in krss-format
   • java -jar mupster.jar -f file.dig -dig (options) for ontologies in dig-format
   where options = [ -u unsatfile ] [-v] [-r] [-o].
   
   It is recommended not to use the -r and -o options.
   The system has been developed and tested under Linux, and there are known problems to run MUPSter under Windows.
   

MUPSTer is experimental software, and you are very likely to get into trouble quickly. If you really consider to play around/work with MUPSter, please contact me, so that I can provide the source code etc.

Benchmark

You can download a set of benchmark terminologies we used for a paper, which is currently under submission, at this location.

Unfortunately, the DICE terminologies is not freely available. Please contact me if you want access.

Benchmark creation software (download here)

Ungzip and tar the file in a directory, which should now contain a directory benchmark/ (with files Benchmark.java and .class), and a file wellington.jar.

These files build a creator for benchmark experiments for debugging of incoherent ontology. The idea is described in a submitted paper; basically, random unfoldable TBoxes are created with different sizes, according to some features that can be given as arguments.

Run the creator with the following command:

java -classpath wellington.jar:. benchmark/Benchmark [options]

OPTIONS

• -dig returns files in dig format (default + krss)
• -cn arg arg is the number of concept names / the TBox size (default = 100)
• -cs arg arg is the maximal size of concepts. (default = 10)
• -r arg arg is the average number of roles (default = 10)
• -dsj arg arg is the ratio of conjunctive/disjunctive concepts (default = 10)
• -n arg arg is the ratio of negative/positive literals (default = 10)
• -e arg arg is the likelihood that an existential quantification occors.(default = 10)

Please contact me for the source of the benchmark creator.