Extracting Unsatisfiable Cores for LTL via Temporal Resolution

Unsatisfiable cores (UCs) are a well established means for debugging in a declarative setting. Still, tools that perform automated extraction of UCs for LTL are scarce. Using resolution graphs to extract UCs is common in many domains. In this paper we construct and optimize resolution graphs for temporal resolution as implemented in the temporal resolution-based solver TRP++ and we use them to extract UCs for propositional LTL. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available.