[Zurück]

M. Baaz, N. Preining:
"Gödel Logics and the Fully Boxed Fragment of LTL";
Vortrag: LPAR-21: 21st. International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Südafrika; 08.05.2017 - 12.05.2017.

In this paper we show that the fully boxed fragment of first-order LTL (which contains only the temporal connective [] (Box) and every atom, every operation but [], and every quantifier is guarded with []) is not recursively enumerable. To obtain incompleteness for this weak fragment we associate to its formulas a corresponding Gödel logic, G_down (an infinitely valued Gödel logic with only one accumulation point of truth values at 0). By embedding the theory of two equivalence relations on finite sets, we show with one proof that the monadic fragments of G_down and G_up (infinitely valued Gödel logic with only one accumulation point of truth values at 1, also the intersection of all finitely valued Gödel logics) with two predicate symbols are not recursively enumerable.

We use arguments from first-order LTL to demonstrate that the complement of the 1-satisfiable formulas of G_down is not recursively enumerable. This is in contrast to the fact that the same fragment for G_up is decidable.