Ordered Resolution with Selection for H(@)

C. Areces and D. Gor\'in. Ordered Resolution with Selection for H(@). In F. Baader and A. Voronkov, editors, Proceedings of LPAR 2004, LNCS, pp. 125–141, Springer, Montevideo, Uruguay, 2005.

Download

[pdf] 

Abstract

The hybrid logic H(@) is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. The resulting logic gains expressive power without increasing the complexity of the satisfiability problem, which remains within PSpace. A resolution calculus for H(@) was introduced in [5], but it did not provide strategies for ordered resolution and selection functions. Additionally, the problem of termination was left open. In this paper we address both issues. We first define proper notions of admissible orderings and selection functions and prove the refutational completeness of the obtained ordered resolution calculus using a standard “candidate model” construction [10]. Next, we refine some of the nominal-handling rules and show that the resulting calculus is sound, complete and can only generate a finite number of clauses, establishing termination. Finally, the theoretical results were tested empirically by implementing the new strategies into HyLoRes [6, 18], an experimental prototype for the original calculus described in [5]. Both versions of the prover were compared and we discuss some preliminary results.

BibTeX

@InCollection{Areces2005a,
  author =       "C. Areces and D. Gor{\'i}n",
  booktitle =    "Proceedings of LPAR 2004",
  title =        "Ordered Resolution with Selection for {H}(@)",
  year =         "2005",
  abstract =     "The hybrid logic H(@) is obtained by adding nominals
                 and the satisfaction operator @ to the basic modal
                 logic. The resulting logic gains expressive power
                 without increasing the complexity of the satisfiability
                 problem, which remains within PSpace. A resolution
                 calculus for H(@) was introduced in [5], but it did not
                 provide strategies for ordered resolution and selection
                 functions. Additionally, the problem of termination was
                 left open. In this paper we address both issues. We
                 first define proper notions of admissible orderings and
                 selection functions and prove the refutational
                 completeness of the obtained ordered resolution
                 calculus using a standard “candidate model”
                 construction [10]. Next, we refine some of the
                 nominal-handling rules and show that the resulting
                 calculus is sound, complete and can only generate a
                 finite number of clauses, establishing termination.
                 Finally, the theoretical results were tested
                 empirically by implementing the new strategies into
                 HyLoRes [6, 18], an experimental prototype for the
                 original calculus described in [5]. Both versions of
                 the prover were compared and we discuss some
                 preliminary results.",
  address =      "Montevideo, Uruguay",
  editor =       "F. Baader and A. Voronkov",
  pages =        "125--141",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       "3452",
  ISBN =         "3-540-25236-3",
}