Alladi Ramakrishnan Hall

Propositional Term Modal Logic

Anantha Padmanabha

IMSc

Public Voa Voce for the Ph.D. degree

Term modal logic (TML) introduced by Fitting, Thalmann and Voronkov in 2001 is one with unboundedly many modalities with quantification over them. In TML we can state properties such as: $\exists x. \forall y. Box_x Box_y alpha$ which may mean: “some agent knows that everybody knows alpha”. The thesis
is a study of technical questions in TML.

We show that even the propositonal fragment of TML is undecidable. We present tight undecidability results and identify some decidable fragments. We introduce the notion of bisimulation for term modal logic and present van Benthem type characterization theorems for several fragments. We discuss complexity of finite model checking and introduce a finite way of specifying infinite models for which the model checking problem is decidable.