MIV for Linux and Windows

MIV (Minimal Interface to Vampire) provides a graphical user interface to the open source version (version 2) of the Vampire Theorem Prover. The interface provides the user with the ability to load KIF (Knowledge Interchange Fomat) or SUO-KIF (Standard Upper Ontology-Knowledge Interachange Format) axioms and present problems to Vampire for evaluation. The system provides formated presentation of the proof generated by Vampire.

MIV screen shot

The Linux Version

Requirements

MIV requires the GTK+ libraries. Your system probably already has these.

MIV has been lightly tested on SUSE SLED 10, and Fedora Core 4.

Installation

  1. Downloaded the compressed tar file: miv-distrib.tgz.
  2. Unpack the file: tar zvxf miv-distrib.tgz This will create a directory ./miv-distrib/
  3. Execute miv-linux.exe and try loading the example KB provided in the subdirectory kb/base.kif See the notes under The 'Help' menu item 'Quick Help' for details about how to run the example.
  4. Let me know if you have any problems: peter.denno@nist.gov

The Windows Version

Requirements

MIV has been lightly tested on Windows 2000 and Windows XP.

Installation

  1. Downloaded the installer: miv-install.exe.
  2. Uninstall all old versions of MIV.
  3. Execute the installer.
  4. If you experience problems running the program, verify that the following user variables are correctly set (Old versions can mess these up. Uninstall may not have cleared them.): The above assumes that you installed in C:/Program Files/MIV You can verify the values of these variables by typing echo %MIVPATH% and echo %PATH%. The latter should show a value that is the concatenation of the system variable Path and the user variable PATH. If this is the case and things still don't work, you can either execute the .exe directly from the shell in which you did the echo, or try rebooting.
  5. Let me know if you have any problems: peter.denno@nist.gov

Changelog

Disclaimer

A more sophisticated Tomcat-based (web-based) interface to Vampire is provided through the Sigma Knowledge Engineering Environment . The purpose of MIV is to provide quick access to the reasoner for exploratory use. It is not a suitable interface for large ontology development.

For more information or questions regarding MIV, please contact Peter Denno.

Disclaimer - This software was produced by the National Institute of Standards and Technology (NIST), an agency of the U.S. government and by statute is not subject to copyright in the United States. Recipients of this software assume all responsibility associated with its operation, modification, maintenance, and subsequent redistribution.

Names of companies and products, and links to commercial pages are provided in order to adequately specify procedures and equipment used. In no case does such identification imply recommendation or endorsement by the National Institute of Standards and Technology, nor does it imply that the products are necessarily the best available for the purpose.