A polyadic dynamic logic is introduced in which a model-theoretic version of nonlocal multicomponent tree-adjoining grammar can be formulated.It is shown to have a low polynomial time model checking procedure.This means that treebanks for nonlocal MCTAG, incl.all weaker extensions of TAG, can be efficiently corrected and queried.Our result is extended to HPSG treebanks (with some qualifications).The model checking procedures can also be used in heuristics-based parsing.* The model checking procedure described in this paper uses constructs from a model checking procedure introduced in joint work with Martin Lange.Thanks also to Laura Kallmeyer, Timm Lichte and Wolfgang Maier for introducing me to various extensions of tree-adjoining grammar, incl.nonlocal MCTAG.