Resolution with Order and Selection for Hybrid Logics

Areces, C. and Gorín, D.. 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: (download)

@ARTICLE{arec:reso08,
  author = {Areces, C. and Gor\'{\i}n, D.},
  title = {Resolution with Order and Selection for Hybrid Logics},
  journal = {Journal of Automated Reasoning},
  year = {2011},
  volume = {46},
  pages = {1-42},
  number = {1},
  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}
}