Some software for public use
RIF BLD tools in Java
RIF BLD abstract syntax package. Create RIF BLD objects, traverse or render them in the presentation syntax. No annotations are supported yet, and rendering can only be done in the presentation syntax.
RIF BLD parser for the XML syntax (updated on Nov 28, 2009).
Converter from RIF BLD to TPTP (updated on Nov 28, 2009). External terms and atoms are not yet supported, and the support for data literals is very experimental.
Contributions are welcome!
Highly reusable TPTP parser in Java can be downloaded from Andrei Tchaltsev's site (a newer version is here)
VampirePrime reasoner
This is an open source reasoner derived from the Sigma KEE edition of Vampire.
C++ sources are here -- should compile OK with Linux and a reasonably fresh version of GCC. You will also need the Expat library. The implementation is very experimental and, generally, only very limited support can be provided.
to Alexandre Riazanov's home page