Is there any mechanization for matching logic (any flavor)?
I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the framework.
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.Sign up to join this community
There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of any formalization covering completeness of matching logic (although there is a pen-and-paper proof in Matching μ-Logic, and a master's thesis).
This formalization is still under development; here is a paper about an earlier (middle of 2022) version of it. The current version covers:
Introduced for proof object generation for the K Framework.
I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti.
More precisely, my work focuses on:
The encodings of Applicative Matching Logic (AML) into Lean and Coq are deep and they want to formalize theoretical results about AML.
Could you tell us why you are interested in mechanizing Matching Logic? The various projects carried out to formalize Matching Logic are not of the same nature, and do not involve the same version of Matching Logic.
Okay, I need to admit that I am not best at googling. It already exists. Seems like the soundness is covered, and completeness only covered for non-mu part.
As for applicative version of matching logic, I did not find anything.