Title: Hybrid Logic Revisited
Author: Moritz Hardt
Advisor: Prof. Dr. Gert Smolka
Location: Saarland University
Year: 2006
Download:
hardt-bathesis.pdf
See also:
Paper version with Gert Smolka.
Electr. Notes Theor. Comput. Sci. 174(6): 15-27 (2007)
Talks:
We present modal logic on the basis of the simply typed lambda calculus with a system of equational deduction. Combining first-order quantification and higher-order syntax, we can maintain modal reasoning in terms of of classical logic by remarkably simple means. Such an approach has been broadly uninvestigated, even though it has notable advantages, especially in the case of Hybrid Logic.
Hybrid logics extend modal languages with the ability to name and identify states in a model, features that have received much attention in many branches of modal logic over the past years. We give natural characterizations of HL(@,downarrow) and its decidable subset HL(@).
We develop a tableau-like decision procedure for our equivalent of HL(@). Our algorithm guarantees termination by local criteria in contrast to previous decision procedures. With regards to deduction, we simplify in particular the treatment of identities. Traditionally, modal tableau calculi either rely on external labeling mechanisms or have to represent access information by equivalent formulas. In our system labeling and access information are both internal and explicit.
The following was a first specific problem description as proposed by Gert Smolka on 8 September, 2005.
In this thesis project you will investigate modal logic (ML) on the basis of higher-order logic (HOL), where both logics are based on the simply typed lambda calculus with equational deduction (S). While we expect that much of the investigation will apply to modal logics in general, linear time logic (LTL), as used in [MP] for system verification, will serve as the standard example. A main goal of the thesis is the development of a higher-order version of LTL. As of now, there is almost no work on higher-order modal logic (but see [F, B]). Our goal is to develop modal logic as a modular extension of HOL that exploits the infrastructure of S and HOL as much as possible. This will be in sharp contrast to existing approaches, which erect modal logic from scratch.
The modal syntax will distinguish between rigid and flexible names (i.e., variables and constants), where the denotation of rigid names is the same at all vertices while the denotation of flexible names depends on vertices.
Fitting [FM] restricts first-order modal quantification to rigid variables, which amounts to first-order classical quantification. First-order LTL [MP] and DL [HKT] provide modal quantification also for flexible variables, which at type A amounts to higher-order classical quantification at type V→A.
Our approach will be based on a type preserving compilation function C that maps modal terms to classical terms. For both modal and classical terms we have equational deduction as provided by S. We want to have a general deductive soundness theorem
(1) A|-e ⇒ CA|-Ce
saying that modal deduction can be simulated by classical deduction. For this to hold beta conversion at the modal side must be restricted since the terms (λx.◊(fx))c and ◊(fc) may denote differently if c is flexible.
The semantics of a particular modal logic L will be described by a set LS of classical equations. The classical models of LS should correspond exactly to the modal models of L, and modal validity should coincide with classical validity:
(2) |= e ⇔ LS |= Ce
Modal deduction for L is to be obtained from a set LA of modal equations so that C(LA) can be deduced classically from LS:
(3) LS |— C(LA)
Together with (1) this yields
(4) LA |— e ⇒ LS |— Ce
If we have semantic modal completeness
(5) |= e ⇒ LA |— e
then deductive modal completeness follows with (2):
(6) LS |— Ce ⇒ LA |— e
[MP] uses many deduction rules and valid formulus for first-order LTL. We will try to devise axiomatizations LS (classical HOL) and LA (modal HOL) from which these rules and formulas can be deduced.
[B] A. Bressan. A General Interpreted Modal Calculus. Yale University Press 1972.
[F] M. Fitting. Higher-order Modal Logic--A Sketch. Springer LNAI 1761, 1998.
[FM] M. Fitting and R.L. Mendelson. First-order Modal Logic. Kluwer 1998.
[HKT] D. Harel, D. Kozen and J. Tiuryn. Dynamic Logic. MIT Press 2000.
[MP] Z. Manna and A. Pnuelli. Temporal Verification of Reactive Systems, Safety. Springer 1995.
Legal notice, Privacy policy