Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting

Christopher Hampson, Agi Kurucz

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various linear t…