We employ a recently developed methodology---called "structural refinement"---to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. Our nested systems incorporate propagation rules, parameterized with formal grammars, that encode certain frame conditions expressible as first-order Horn formulae and which correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules.
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement