Previous automated approaches to discovering design patterns in source code have suffered from a need to enumerate static descriptions of structural and behavioural relationships, resulting in a finite library of variations on pattern implementation. Our approach, System for Pattern Query and Recognition, or SPQR, differs in that we do not seek statically to encode each variant of the patterns that we wish to find. Our system finds pattern variants that were not explicitly defined, but instead are inferred dynamically during code analysis by a theorem prover, providing practical tool support for software construction, comprehension, maintenance, and refactoring. We use a logical inference system to reveal large numbers of patterns and their variations from a small number of definitions by encoding in a formal denotational semantics a small number of fundamental OO concepts (elemental design patterns), encode the rules by which these concepts are combined to form patterns (reliance operators), and encode the structural/behavioral relationships among components of objects and classes (rho-calculus). A chain of fully automated tools provides a path from source code to revealed patterns.We describe our approach in this paper with a concrete example to drive the discussion, accompanied by formal treatment of the foundational topics.