HyLoRes: A Hybrid Logic Prover Based on Direct Resolution

C. Areces and J. Heguiabehere. HyLoRes: A Hybrid Logic Prover Based on Direct Resolution. In Proceedings of Advances in Modal Logic 2002, Toulouse, France, 2002.

Download

[pdf] 

Abstract

In recent years, an important number of theoretical results concerning axiomatizability, proof systems (e.g., tableaux, natural deduction), interpolation, expressive power, complexity, etc. for hybrid logics have 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).

BibTeX

@InProceedings{Areces2002c,
  author =       "C. Areces and J. Heguiabehere",
  booktitle =    "Proceedings of Advances in Modal Logic 2002",
  title =        "HyLoRes: {A} Hybrid Logic Prover Based on Direct
                 Resolution",
  year =         "2002",
  abstract =     "In recent years, an important number of theoretical
                 results concerning axiomatizability, proof systems
                 (e.g., tableaux, natural deduction), interpolation,
                 expressive power, complexity, etc. for hybrid logics
                 have 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).",
  address =      "Toulouse, France",
}