Second-order Propositional Modal Logic: Expressiveness and Completeness Results



Belardinelli, Francesco, Van Der Hoek, Wiebe and Kuijer, Louwe B ORCID: 0000-0001-6696-9023
(2018) Second-order Propositional Modal Logic: Expressiveness and Completeness Results. Artificial Intelligence, 263. pp. 3-45.

This is the latest version of this item.

[img] Text
submission.pdf - Submitted version

Download (934kB)
[img] Text
version_that_was_accepted.pdf - Author Accepted Manuscript

Download (750kB)

Abstract

In this paper we advance the state-of-the-art on the application of second-order propositional modal logic (SOPML) in the representation of individual and group knowledge, as well as temporal and spatial reasoning. The main theoretical contributions of the paper can be summarised as follows. Firstly, we introduce the language of (multi-modal) SOPML and interpret it on a variety of different classes of Kripke frames according to the features of the accessibility relations and of the algebraic structure of the quantification domain of propositions. We provide axiomatisations for some of these classes, and show that SOPML is unaxiomatisable on the remaining classes. Secondly, we introduce novel notions of (bi)simulations and prove that they indeed preserve the interpretation of formulas in (the universal fragment of) SOPML. Then, we apply this formal machinery to study the expressiveness of Second-order Propositional Epistemic Logic (SOPEL) in representing higher-order knowledge, i.e., the knowledge agents have about other agents' knowledge, as well as graph-theoretic notions (e.g., 3-colorability, Hamiltonian paths, etc.). The final outcome is a rich formalism to represent and reason about relevant concepts in artificial intelligence, while still having a model checking problem that is no more computationally expensive than that of the less expressive quantified boolean logic.

Item Type: Article
Uncontrolled Keywords: Modal logic, Knowledge representation, Second-order propositional modal logic, Epistemic logic, Local properties
Depositing User: Symplectic Admin
Date Deposited: 17 Jul 2018 07:43
Last Modified: 19 Jan 2023 01:30
DOI: 10.1016/j.artint.2018.07.004
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3023833

Available Versions of this Item