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.

Our TODO list includes:

  • Make the prover aware of the characteristics of its input (ongoing).
  • Extend the language with the universal modality A, which will let us perform inference in terms of full Boolean knowledge bases of the description logic ALC, in HyLoRes.
  • Display a concise refutation proof in case it finds one.

Download

The haskell source can be downloaded from