HyLoRes: A Resolution Based Theorem Prover for Hybrid Logics
HyLoRes is a direct resolution prover for hybrid logics. These are modal-like logics with facilities to refer to objects in a model.
The most interesting distinguishing feature of HyLoRes is that it is not based on tableau algorithms but on (direct) resolution. HyLoRes performs resolution directly on the modal (or hybrid) input, with no translation into background logics.
HyLoRes fuses state-of-the-art first-order proving ideas with the simple representation of the hybrid object language.
Main Features
- Apart from the classic operators of the basic modal logic K, HyLoRes can handle nominals, the satisfaction operator @, the down arrow binder and the inverse (aka «past») modality.
- It can generate a model from the saturated set when the input formula is satisfiable.
The Implementation
HyLoRes is implemented in Haskell, and the executable is generated using the Glasgow Haskell Compiler.
Documentation
Download
Stable version
Development version
Building from the source and installing
To install HyLoRes in your home directory, you first need to install hylolib in your home directory. Then, get the source code of HyLoRes, and if you have installed the Haskell Platform or cabal-install, then you can install HyLoRes by going in the directory containing the file hylores.cabal and doing:
cabal install
The binary will be located in $HOME/.cabal/bin
