[Zurück]

M. Baaz, N. Preining:
"Gödel logics and the fully boxed fragment of LTL";
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 46 (2017), S. 404 - 416.

In this paper we show that a very basic fragment of FO-LTL, the monadic fully boxed fragment (all connectives and quantifiers are guarded by P) is not recursively enumerable wrt validity and 1-satisfiability if three predicates are present. This result is obtained by reduction of the fully boxed fragment of FO-LTL to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in [0,1] such that all but 0 are isolated. The result on 1-satisfiability is in no way symmetric to the result on validity as in classical logic: this is demonstrated by the analysis of G↑, the related infinitely-valued Gödel logic with truth values in [0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at least two predicates is not recursively enumerable, 1-satisfiability of the monadic fragment is decidable.

Gödel logic, LTL, monadic fragment

http://dx.doi.org/10.29007/bdbm