Revisiting the Fluted and Forward Fragments with Guards
摘要
The guarded fluted (forward) fragment is the intersection of the guarded fragment and the fluted (forward) fragment of first-order logic. In this paper we showcase a simple and special model construction technique which turns each first-order structure into a modal structure and back. Based on that, we devise a translation of the two guarded fragments to the basic modal logic extended with the universal modality, providing a simulation of the guarded fluted fragment as well as a new proof of the ExpTime-completeness of the satisfiability problem. Moreover, our technique induces a variant of the unraveling construction. As an application of the unraveling, we prove the Łoś-Tarski Preservation Theorem in the two fragments.