Maude and its formal tools support ten different symbolic computation features. This paper focuses on one of them, narrowing of constrained patterns, as well as its combination with inductive theorem proving in a novel style of deductive model checking, to illustrate how Maude’s symbolic features can be used to model check modal logic properties of infinite-state systems specificed as rewrite theories in Maude.