Nonaxiomatizability and undecidability of an infinite-valued temporal logic
An infinite-valued propositional temporal logic ITL with operators "nexttime", "sometimes" and "always" is defined. ITL is based on a strong notion of satisfiability and a weak notion of validity. By reducing the halting problem and also the complement of the halting problem of specialized two-counter machines to the satisfiability problem of ITL it is shown that this temporal logic ITL is neither decidable nor axiomatizable.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten