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.
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
- Downloaded the compressed tar file: miv-distrib.tgz.
- Unpack the file: tar zvxf miv-distrib.tgz
This will create a directory ./miv-distrib/
- 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.
- 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
- Downloaded the installer: miv-install.exe.
- Uninstall all old versions of MIV.
- Execute the installer.
- 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.):
- MIVPATH C:/Program Files/MIV/
- PATH should contain C:/Program Files/MIV/GTK/2/bin.
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.
- Let me know if you have any problems: peter.denno@nist.gov
Changelog
- 2007-04-20 Fixed problem crashing if do 'ask' after a bad ontology parse. Allow symbols to start with - (dash) (or just -).
- 2007-04-17 Fixed problem reading 'special characters.'
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.