OWL DL Satisfiability Model Visualization Plugin for Protege


SatModViz is a plugin for Protege that displays a minimal satisfiability model for the currently loaded ontology in "music score notation".

This plugin requires Mace4 FOL finite model builder installed on the system in advance.

This is an incomplete and experiemental (proof of concept) implementation only!!! A proper way to implement this plugin would be to modify one of OWL DL / OWL 1.1. reasoners (Pellet or FaCT++) to directly output the Satisfiability Model - we are seeking a competent volunteer for this task ;-) Also the visualisation itself would benefit from adding some filtering tools.

Downloading and Installing

You can download a binary distribution here (7.6 MB). Just unzip this archive and place the directory "" in your Protege/plugins subdirectory and activate the plugin in the "Projects->Configure" menu of Protege application. The first thing you'll be asked is to show the exact location of the Mace4 FOL model builder. Here is a simple pizza ontology for testing the plugin.

Building from source

The plugin source code (the Ant project) is also available:

  1. You'll have to download additional dependencies though:
  2. Place the *.jar files from both libraries in directories lib/batik and lib/velocity of your downloaded source code tree.
  3. Copy files looks-*.jar, protege.jar and protege.jar from your Protege directory into lib/protege direcotory
  4. Copy all *.jar files from your Protege/plugins/edu.stanford.smi.protegex.owl directory into the lib/protege-owl directory
  5. Edit file to set the correct Protege location.
  6. Execute command ant protege-deploy to compile and install the plugin


Martins Barinskis (martins.barinskis at gmail dot com)
Guntis Barzdins (guntis.barzdins at mii dot lu dot lv)
Institute of Mathematics and Computer Science
University of Latvia