DYNAMIC BITS AND PIECES

Abstract

Arrow Logic remains PSPACE-complete. Further arrow axioms can easily lead to 36 undecidability. (In private correspondence, Marx has also announced EXP-TIME complexity for the original Guarded Fragment, via a reduction to CRS over 'locally cube' models.) Marx and Venema 1996 is a systematic state-of-the-art presentation of many-dimensional modal logic, including bridges with algebraic logic, as well as many key techniques for dynamic logic, broadly conceived. Ter Meulen 1995 proposes a concise framework for temporal representation in natural language that may be viewed as an alternative dynamification of temporal logic, using an extra, intermediate level of representation. Successive formulas algorithmically generate successive 'dynamic aspect trees', for which there is a notion of 'succesful embedding' into standard temporal models. Valid inference can then be defined as verification of the conclusion by any succesful embedding for the DAT of the premise sequence. This alternative d...