We advance an institutional formalisation of the logical systems that underlie the K semantic framework and are used to capture both structural properties of program configurations through pattern matching, and changes of configurations through reachability rules. By defining encodings of matching and reachability logic into the institution of first-order logic, we set the foundation for integrating K into logic graphs of heterogeneous institution-based specification languages such as HETCASL. This will further enable the use of the K tool with other existing formal specification and verification tools associated with Hets.