This book stands at the intersection of two topics: the
decidability and computational complexity of hybrid logics, and the
deductive systems designed for them. Hybrid logics are here divided
into two groups: standard hybrid logics involving nominals as
expressions of a separate sort, and non-standard hybrid logics,
which do not involve nominals but whose expressive power matches
the expressive power of binder-free standard hybrid logics.The
original results of this book are split into two parts. This
division reflects the division of the book itself. The first type
of results concern model-theoretic and complexity properties of
hybrid logics. Since hybrid logics which we call standard are quite
well investigated, the efforts focused on hybrid logics referred to
as non-standard in this book. Non-standard hybrid logics are
understood as modal logics with global counting operators (M(En))
whose expressive power matches the expressive power of binder-free
standard hybrid logics. The relevant results comprise: 1.
Establishing a sound and complete axiomatization for the modal
logic K with global counting operators (MK(En)), which can be
easily extended onto other frame classes, 2. Establishing tight
complexity bounds, namely NExpTime-completeness for the modal logic
with global counting operators defined over the classes of
arbitrary, reflexive, symmetric, serial and transitive frames
(MK(En)), MT(En)), MD(En)), MB(En)), MK4(En)) with numerical
subscripts coded in binary. Establishing the exponential-size model
property for this logic defined over the classes of Euclidean and
equivalential frames (MK5(En)), MS5(En)).Results of the second type
consist of designing concrete deductive (tableau and sequent)
systems for standard and non-standard hybrid logics. More
precisely, they include: 1. Devising a prefixed and an internalized
tableau calculi which are sound, complete and terminating for a
rich class of binder-free standard hybrid logics. An interesting
feature of indicated calculi is the nonbranching character of the
rule (ŹD), 2. Devising a prefixed and an internalized tableau
calculi which are sound, complete and terminating for non-standard
hybrid logics. The internalization technique applied to a tableau
calculus for the modal logic with global counting operators is
novel in the literature, 3. Devising the first hybrid algorithm
involving an inequality solver for modal logics with global
counting operators. Transferring the arithmetical part of reasoning
to an inequality solver turned out to be sufficient in ensuring
termination.The book is directed to philosophers and logicians
working with modal and hybrid logics, as well as to computer
scientists interested in deductive systems and decision procedures
for logics. Extensive fragments of the first part of the book can
also serve as an introduction to hybrid logics for wider audience
interested in logic.The content of the book is situated in the
areas of formal logic and theoretical computer science with some
elements of the theory of computational complexity.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!