Model Checking and Validity in Propositional and Modal Inclusion Logics

TL;DR

This paper analyzes the complexity of model checking and validity in propositional and modal inclusion logics, advancing the classification of reasoning problems within team semantics-based logics.

Contribution

It establishes complexity bounds for model checking and validity under lax and strict semantics, progressing towards a comprehensive complexity classification.

Findings

Complexity bounds identified for model checking.

Complexity bounds identified for validity.

Progress towards classifying reasoning problems in dependence and inclusion logics.

Abstract

Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the central reasoning problems for modal and propositional dependence, independence, and inclusion logics.