Ian Hodkinson: ISO, MSc/MRes project suggestions
I am happy to discuss suggestions for ISOs and MSc projects in modal and temporal
logic, and in hybrid logic and algebraic logic. Some could be developed into a
summer individual project or even a Ph.D.
Good mathematical
ability and an interest in mathematical proofs will help.
Previous work
Work done in previous ISOs and projects with me has led to the following publications and distinguished projects.
Several others attained Distinction level and made important advances.
Apologies if some links above are broken - they change frequently.
Some sample topics
Please contact me if you have your own ideas instead.
- Canonicity in modal logic
A modal logic is canonical
if it is valid in the frame of its own
canonical model. Showing a logic to be canonical is a key method
of proving completeness for it, and a great deal of research
has been done on canonicity. Canonicity is sometimes discussed a little
in course 499 Modal and Temporal
Logic, but it could be taken
much further in an ISO or project.
- canonicity of simple logics.
- Fine's theorem that the modal logic of an elementary class
of frames (a class defined by first-order sentences) is canonical.
(See K. Fine, Some connections between elementary and modal logic,
in Proc. 3rd Scandinavian logic symposium, S. Kanger (ed.),
North Holland, 1975, pp.15-31, and J. van Benthem, Canonical
modal logics and ultrafilter extensions, J. Symbolic Logic 44 (1979) 1-8.)
- converse of Fine's theorem?
- algebraic versions of canonicity. Work of Jónsson and
Tarski. Extensions to lattices?
- non-canonical logics. McKinsey axiom.
- Barely canonical logics (e.g., McKinsey-Lemmon logic, Hughes's logic).
- Extending canonicity to Heyting algebras, lattices, etc.
As an ISO, this would be best run
in term 2. Prerequisite: course 499.
- Sahlqvist's theorem
This is a core area of modal logic. We prove Sahlqvist correspondence
in course 499 Modal and Temporal Logic, but
it has a big sister, Sahlqvist's completeness
theorem, that we do not go into. Various topics are possible:
- Canonicity and Sahlqvist's completeness theorem.
- Extensions (e.g., by Conradie--Goranko--Vakarelov, Kikot, ...):
canonicity and/or correspondence could be looked at.
- Sahlqvist for the mu-calculus
- More general version via hybrid logic.
- Hybrid logic
This is an extension of modal logic made by adding nominals --
special propositional atoms that are true at exactly one world, and serve to name that world.
This makes the logic more expresive (and raises its computational complexity).
Hybrid logic is a quite active area of research. An ISO or project could look into basic hybrid logics,
their expressiveness, and some completeness theorems.
See hybrid logic home page.
The paper What are hybrid languages? by Blackburn and Seligman is a fair place to start.
The papers with
Paternault and
Tahiri
mentioned at the top arose from an MSc project and ISO
(respectively) on this topic.
Prerequisite: course 499.
- Complexity of modal and
temporal
logics
This fills something of a gap in course 499 Modal and Temporal
Logic.
Because students may not have done any complexity before,
we don't cover complexity in the course. However, the
reasonable complexity of modal and temporal logics
is often claimed as a key plus point for using
them in applications. So if you have done/are doing MTL
and also course 438 Complexity, you may be interested in looking
into the decidability and complexity of these logics. This will
reinforce both courses.
The field
is large and there are many possible topics. An ISO or project could look at
many of them in outline, or one or two in depth. Some
examples:
- PSPACE-completeness for the basic modal logics K, K4, S4.
References:
Richard E. Ladner, The Computational Complexity of Provability in Systems of
Modal Propositional Logic, Siam J. Comput. Vol. 6, No. 3, September 1977.
Also see Edith Spaan's article in
Diamonds and defaults: studies in pure and applied intensional logic,
edited by Maarten de Rijke, Kluwer Academic Publishers, 1993.
(This book is in the library).
- temporal logic: proofs of complexity
and finite model property of linear modal and temporal logics,
and of PSPACE-completeness for Until and Since over the natural numbers.
References:
Hiroakira Ono and Akira Nakamura,
On the size of refutation Kripke models for some linear modal and tense logics,
Studia Logica Volume 39, Number 4, December 1980.
A P Sistla, E M Clarke, The complexity of propositional linear temporal
logics, Journal of the ACM (JACM), vol.32 no.3, July 1985, pp.733-749.
- decidable ('monodic') fragments of first-order temporal logic
--- complexity too. Konstantinos Mamouras did a
distinguished project on this topic in 2009,
which is unlikely to be improved on.
- links to (decidable) guarded fragments of first-order
logic. Vardi's thesis that modal logics are robustly
decidable.
- the view of others such as Zakharyaschev that modal logics
are robustly undecidable
- complexity of hybrid logics
- high complexity (up to and including non-primitive
recursive complexity) and undecidability of products and related
systems (such as with expanding domains).
This is probably too much for an ISO
and may be best left for a project or Ph.D.
As an ISO, this would definitely run in term 2.
Prerequisites: (1) course 499, (2)
you should preferably be taking course 438 -- definitely so if you
haven't done space complexity before.
- Algebraic logic
This is a variant of modal logic. It looks at modal logic from
'the other side', giving algebraic versions of modal logics based on
Boolean algebras with operators.
- basics of BAOs; the work of Jónsson and Tarski.
- formulas as terms. Varieties and modal logics
- Birkhoff's (and Tarski's) theorem: Var(K) = HSP(K)
- examples; Kripke-incomplete logics; algebraic semantics via general frames.
A more specific subtopic would be
relation algebras --- see, e.g., this
book.
Prerequisite: course 499.
- Expressive completeness in temporal logic
This is about comparing the expressiveness of temporal
and first-order logic. Surprisingly, they are sometimes
equally expressive. The proofs are tough.
- Kamp's theorem: Until and Since are expressively complete
over dedekind complete linear time
- extension to arbitrary linear time: Stavi connectives
- perhaps tree-like time too
- H-dimension, k-variable property. Circular time
- Gabbay's separation property
- ??completeness via completeness??
- interval temporal logics: positive results for CDT logic; Venema's negative results
- the first-order case over linear time --- some positive results, some negative
- partially analogous modal results: van Benthem's bisimulation theorem
- More recent results of Hirschfeld, Hunter, Ouaknine, Rabinovich, Worrell
Term 2 only. Prerequisite: course 499.
- Interval temporal logic
This is based on periods of time, rather than time points. Work of
van Benthem, Goranko, Halpern & Shoham, Hussain, Lodaya, Sciavicco, Venema, ... could be looked at.
- Different systems
- Axiomatisations, expressiveness, complexity
- Spatial logic
The topological ('spatial') interpretation of
modal operators predates Kripke semantics but is enjoying a new
surge of interest. Work of Lucero-Bryan, McKinsey-Tarski, Shehtman,
and others could be looked at.
- Other important results in modal logic:
- Goldblatt-Thomason theorem (as above)
- van Benthem's bisimulation theorem
- Bull's and Fine's theorems on logics above S4.3
- zero-one laws: work of Le Bars
(and Halpern--Kapron)
- etc
Term 2 only. Prerequisite: course 499.