Skip to main content

Mechanised modal model theory


Michael Norrish and Yiming Xu



Australian National University


In this paper, we discuss the formalisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in formalisations of modal logic have centered on proof systems and applications in model-checking. We have formalised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al.). Among others, one important result, the Van Benthem characterisation theorem, characterizes the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters.

BibTeX Entry

    author           = {Norrish, Michael and Xu, Yiming},
    doi              = {\_30},
    month            = jul,
    date             = {2020-7-1},
    year             = {2020},
    title            = {Mechanised Modal Model Theory},
    address          = {Paris},
    pages            = {518-533},
    booktitle        = {International Joint Conference on Automated Reasoning},
    publisher        = {Springer}