Kernkonzepte
Model checking complexity for inquisitive logics is proven to be PSPACE-complete.
Zusammenfassung
The paper studies the complexity of model checking problems for inquisitive propositional logic InqB and modal logic InqM, proving them to be AP-complete. It introduces inquisitive logics, information models, and semantics. The study includes a reduction of the TQBF problem to MC(InqB), establishing PSPACE-completeness.
Introduction:
Studies model checking complexity for InqB and InqM.
Defines inquisitive logics extending classical logic with questions.
Preliminaries:
Information models defined for InqB and InqM.
Semantics based on information states supporting statements/questions.
Encoding and Model Checking Algorithm:
Switching models used to encode Boolean valuations.
Special formulas introduced to encode TQBF problem into MC(InqB).
Complexity of Model Checking for InqB:
Reduction of TQBF problem to MC(InqB) proves PSPACE-completeness.
Statistiken
In recent years, the problem has been addressed also for a class of logics called team logics which, like our inquisitive systems, are interpreted relative to sets of assignments (see, e.g., [5, 6] and [9, Ch. 7]).
Both MC(InqB) and MC(InqM) are PSPACE-complete.