Resolution with Order and Selection for Hybrid Logics

C. Areces and D. Gor\'in. Resolution with Order and Selection for Hybrid Logics. Journal of Automated Reasoning, 46(1):1–42, 2011.

Download

[pdf] 

Abstract

We investigate labeled resolution calculi for hybrid logics with inference rules restricted via selection functions and orders. We start by providing a sound and refutationally complete calculus for the hybrid logic H(@, \downarrow, A), even under restrictions by selection functions and orders. Then, by imposing further restrictions in the original calculus, we develop a sound, complete and terminating calculus for the H (@) sublanguage. The proof scheme we use to show refutational completeness of these calculi is an adaptation of a standard completeness proof for saturation-based calculi for first-order logic that guarantees completeness even under redundancy elimination. In fact, one of the contributions of this article is to show that the general framework of saturation-based proving for first-order logic with equality can be naturally adapted to saturation-based calculi for other languages, in particular modal and hybrid logics.

BibTeX

@Article{Areces2011e,
  author =       "C. Areces and D. Gor{\'i}n",
  journal =      "Journal of Automated Reasoning",
  title =        "Resolution with Order and Selection for Hybrid
                 Logics",
  year =         "2011",
  number =       "1",
  pages =        "1--42",
  volume =       "46",
  abstract =     "We investigate labeled resolution calculi for hybrid
                 logics with inference rules restricted via selection
                 functions and orders. We start by providing a sound and
                 refutationally complete calculus for the hybrid logic
                 H(@, \downarrow, A), even under restrictions by
                 selection functions and orders. Then, by imposing
                 further restrictions in the original calculus, we
                 develop a sound, complete and terminating calculus for
                 the H (@) sublanguage. The proof scheme we use to show
                 refutational completeness of these calculi is an
                 adaptation of a standard completeness proof for
                 saturation-based calculi for first-order logic that
                 guarantees completeness even under redundancy
                 elimination. In fact, one of the contributions of this
                 article is to show that the general framework of
                 saturation-based proving for first-order logic with
                 equality can be naturally adapted to saturation-based
                 calculi for other languages, in particular modal and
                 hybrid logics.",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
  ee =           "http://dx.doi.org/10.1007/s10817-010-9167-0",
}