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.