The fluted fragment with transitive relations |
| |
Institution: | 1. University of Opole, Poland;2. University of Manchester, UK;3. University of Opole, Institute of Computer Science, Oleska 48, 45-052 Opole, Poland |
| |
Abstract: | The fluted fragment is a fragment of first-order logic (without equality) in which, roughly speaking, the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that this fragment has the finite model property. We consider extensions of the fluted fragment with various numbers of transitive relations, as well as the equality predicate. In the presence of one transitive relation (together with equality), the finite model property is lost; nevertheless, we show that the satisfiability and finite satisfiability problems for this extension remain decidable. We also show that the corresponding problems in the presence of two transitive relations (with equality) or three transitive relations (without equality) are undecidable, even for the two-variable sub-fragment. |
| |
Keywords: | Fluted logic Transitivity Satisfiability Decidability |
本文献已被 ScienceDirect 等数据库收录! |
|