HyLoRes: A Hybrid Logic Prover Based on Direct Resolution
Carlos Areces, Juan Heguiabehere

Abstract:
In recent years, an important number of theoretical results concerning
axiomatizability, proof systems (tableaux, natural deduction, etc.),
interpolation, expressive power, complexity, etc. for hybrid logics
has been obtained.  The next natural step is to develop provers that
can handle these languages.  HyLoRes is a direct resolution prover for
hybrid logics implementing a sound and complete algorithm for
satisfiability of sentences in H(@,\downarrow).  The most interesting
distinguishing feature of HyLoRes is that it is not based on tableau
algorithms but on (direct) resolution.