Complexity of the interpretability logic IL

TL;DR

This paper proves that the decision problem for the basic interpretability logic IL is PSPACE-complete by presenting a polynomial-space algorithm and establishing its hardness.

Contribution

It establishes the PSPACE-completeness of the interpretability logic IL decision problem and provides a polynomial-space algorithm for it.

Findings

Decision problem for IL is PSPACE-complete

Presented a polynomial-space decision algorithm for IL

Confirmed PSPACE-hardness of IL's closed fragment

Abstract

We show that the decision problem for the basic system of interpretability logic IL is PSPACE-complete. For this purpose we present an algorithm which uses polynomial space with respect to the complexity of a given formula. The existence of such algorithm, together with the previously known PSPACE hardness of the closed fragment of IL, implies PSPACE-completeness.