This tool 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.

Interested users:
 *    Download the program (available for MS Windows only) [ miv-install.exe ]

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.

Send questions or comments to Webmaster.
Date Created: February 8, 2006
Last Modified: February 27, 2006