Some software for public use

Alabai - an experimental resolution- and paramodulation-theorem prover in Java: GitHub repository. This is a guinea pig for experiments with new architectural ideas for resolution- and paramodulation-theorem proving and the Incremental Query Rewriting method for expressive semantic querying of relational data and RDF.

Logic Warehouse - a reusable Java library of data structures and algorithms for first-order logic (underlies Alabai): GitHub repository.

Highly reusable TPTP parser in Java: GitHub repository.



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.



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.



to Alexandre Riazanov's home page