Automated reasoning techniques for hybrid logics

Abstract : Hybrid logics augment classical modal logics with machinery for describing and reasoning about identity, which is crucial in many settings. Although modal logics we would today call ``hybrid'' can be traced back to the work of Prior in the 1960's, their systematic study only began in the late 1990's. Part of their interest comes from the fact they fill an important expressivity gap in modal logics. In fact, they are sometimes referred to as ``modal logics with equality''. One of the unifying themes of this thesis is the satisfiability problem for the arguably best-known hybrid logic, H(@,dwn), and some of its sublogics. Satisfiability is the basic problem in automated reasoning. In the case of hybrid logics it has been studied fundamentally using the tableaux method. In this thesis we attempt to complete the picture by investigating satisfiability for hybrid logics using first-order resolution (via translations) and variations of a resolution calculus that operates directly on hybrid formulas. We present firstly several satisfiability-preserving, linear-time translations from H(@,dwn) to first-order logic. These are conceived in a way such that they tend to reduce the search space of a resolution-based theorem prover for first-order logic. We then move our attention to resolution-based calculi that work directly on hybrid formulas. In particular, we will consider the so-called direct resolution calculus. Inspired by first-order logic resolution, we turn this calculus into a calculus of ordered resolution with selection functions and prove that it possesses the reduction property for counterexamples from which it follows its completeness and that it is compatible with the well-known standard redundancy criterion. We also show that certain refinement of this calculus constitutes a decision procedure for H(@), a decidable fragment of H(@,dwn). In the last part of this thesis we investigate certain normal forms for hybrid logics and other extended modal logics. We are interested in normal forms where certain modalities can be guaranteed not to occur under the scope of other modal operators. We will see that these kind of transformations can be exploited in a pre-processing step in order to reduce the number of inferences required by a modal prover. In an attempt to formulate these results in a way that encompasses also other extended modal logics, we arrived at a formulation of modal semantics in terms of a novel type of models that are coinductively defined. Many extended modal logics (such as hybrid logics) can be defined in terms of classes of coinductive models. This way, results that had to be proved separately for each different language (but whose proofs were known to be mere routine) now can be proved in a general way.
Document type :
Theses
Complete list of metadatas

Cited literature [88 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748220
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:28:52 AM
Last modification on : Tuesday, April 24, 2018 - 1:53:20 PM
Long-term archiving on: Friday, September 14, 2018 - 12:08:35 AM

File

SCD_T_2009_0131_GORIN.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748220, version 1

Collections

Citation

Daniel Alejandro Gorín. Automated reasoning techniques for hybrid logics. Other [cs.OH]. Université Henri Poincaré - Nancy 1, 2009. English. ⟨NNT : 2009NAN10131⟩. ⟨tel-01748220⟩

Share

Metrics

Record views

28

Files downloads

22