Cargando…
Mechanised Modal Model Theory
In this paper, we discuss the mechanisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have mechanised a number of fundamental results from th...
Autores principales: | , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324286/ http://dx.doi.org/10.1007/978-3-030-51074-9_30 |
_version_ | 1783551909387304960 |
---|---|
author | Xu, Yiming Norrish, Michael |
author_facet | Xu, Yiming Norrish, Michael |
author_sort | Xu, Yiming |
collection | PubMed |
description | In this paper, we discuss the mechanisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have mechanised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al. [1]). Among others, one important result, the Van Benthem characterisation theorem, characterises the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters. |
format | Online Article Text |
id | pubmed-7324286 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73242862020-06-30 Mechanised Modal Model Theory Xu, Yiming Norrish, Michael Automated Reasoning Article In this paper, we discuss the mechanisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have mechanised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al. [1]). Among others, one important result, the Van Benthem characterisation theorem, characterises the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters. 2020-05-30 /pmc/articles/PMC7324286/ http://dx.doi.org/10.1007/978-3-030-51074-9_30 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic. |
spellingShingle | Article Xu, Yiming Norrish, Michael Mechanised Modal Model Theory |
title | Mechanised Modal Model Theory |
title_full | Mechanised Modal Model Theory |
title_fullStr | Mechanised Modal Model Theory |
title_full_unstemmed | Mechanised Modal Model Theory |
title_short | Mechanised Modal Model Theory |
title_sort | mechanised modal model theory |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324286/ http://dx.doi.org/10.1007/978-3-030-51074-9_30 |
work_keys_str_mv | AT xuyiming mechanisedmodalmodeltheory AT norrishmichael mechanisedmodalmodeltheory |