The Complexity of Probabilistic Justification Logic

TL;DR

This paper introduces a tableau decision procedure for probabilistic justification logic, establishing its satisfiability can be decided in polynomial space and proving this bound is optimal.

Contribution

It presents a polynomial-space tableau method for probabilistic justification logic and proves the tightness of this complexity bound.

Findings

Decidability of satisfiability in probabilistic justification logic

Polynomial-space tableau decision procedure

Optimality of the complexity bound

Abstract

Probabilistic justification logic is a modal logic with two kind of modalities: probability measures and explicit justification terms. We present a tableau procedure that can be used to decide the satisfiability problem for this logic in polynomial space. We show that this upper complexity bound is tight.