# From Hybrid Modal Logic to Matching Logic and Back

## TL;DR

This paper establishes a formal correspondence between hybrid modal logic and Matching Logic, enabling the transfer of theoretical results and enhancing the capabilities of both frameworks for program specification and verification.

## Contribution

It introduces modal logic equivalents for Matching Logic, facilitating cross-system transfer of results and insights.

## Key findings

- Established formal equivalences between hybrid modal logic and Matching Logic
- Demonstrated how results can be transferred between the two logical systems
- Enhanced understanding of the relationship between modal logic and program verification

## Abstract

Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which should benefit both systems.