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.
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
1
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).
Applicative Matching Logic in Coq
This formalization is still under development; here is a paper about an earlier (middle of 2022) version of it. The current version covers:
- Syntax (using the locally nameless encoding of binders) including mu; semantics; proof system.
- Soundness of the proof system.
- A "proof mode" on top of the proof system - a set of tactics for constructing matching logic proofs interactively.
- Theory of definedness/equality (both from a model-theoretical and proof-theoretical perspective).
- Theory of sorts and natural numbers.
- Many proof system theorems from Matching μ-Logic, adapted to AML.
- Deduction theorem - a proof (of the most general variant available in a technical report accompanying the above-linked Matching μ-Logic paper), as well as an infrastructure for using that theorem.
- Some other model theory (isomorphisms, "model extension").
Applicative Matching Logic in Lean
- Syntax (using named encoding of binders) including mu; semantics; proof system.
- Soundness of the proof system.
- Proof extraction into Metamath (see the Metamath-based formalization below).
- Deduction theorem for closed patterns.
Applicative Matching Logic in Metamath
Introduced for proof object generation for the K Framework.
- Syntax (using named encoding of binders) including mu.
- Proof system.
- Lots of lemmas using the proof system.
A Translator from K into Dedukti
-
1$\begingroup$ Note that the Metamath proof generation includes a translation from K's kore to Matching Logic. Unfortunately it is not too well documented. github.com/runtimeverification/proof-generation/tree/main/src/… $\endgroup$ Aug 16 at 14:07
$\begingroup$
$\endgroup$
2
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 translation from K into Dedukti that you mention (probably because you found this paper: https://doi.org/10.4230/LIPIcs.TYPES.2022.12) is based on the translation from K into Matching Logic. Your translation interprets the Matching Logic operators to be able to execute programs into Dedukti.
- A shallow encoding from Matching mu-Logic is available here: https://gitlab.com/semantiko/ML2DK (need to be updated). This encoding is a first step to recheck KProver proofs into Dedukti.
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.
-
$\begingroup$ I am interested for several reasons. 1. To understand matching logic better (cuz it is not very clear, which statements on that are proved, and how it compares to more well known logics) 2. To understand how (parametrized?) soundess/completeness usually look. $\endgroup$– uhbif19Sep 8 at 16:15
-
$\begingroup$ Your work direction is very interesting BTW, I was heard of it before. $\endgroup$– uhbif19Sep 8 at 16:16
$\begingroup$
$\endgroup$
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.
https://arxiv.org/abs/2201.05716
As for applicative version of matching logic, I did not find anything.