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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Revisiting the Fluted and Forward Fragments with Guards

  • Hongkai Yin

摘要

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.