Difference between revisions of "Open Problems in Matching Logic"
(Created page with "Here are some interesting open problems in matching logic (ML) and its extension matching mu-logic (MmL), listed in no particular order. <!--Feel free to contact me ([[Xiaoho...")
Latest revision as of 07:09, 14 July 2019
Here are some interesting open problems in matching logic (ML) and its extension matching mu-logic (MmL), listed in no particular order.
The following papers are the canonical ones about ML and MmL. We will refer to the first paper as the ML paper, and the second paper as the MmL paper, respectively.
- Matching mu-Logic
- Xiaohong Chen and Grigore Rosu
LICS'19. 2019. To appear
PDF, Matching Logic, LICS'19, BIB
OP1. Global completeness of ML
Recall that the formulas of ML, called patterns, evaluate to the sets of elements that match them. This is different from first-order logic (FOL), where formulas evaluate to only two possible values: true or false. It is more similar to modal logic, where formulas evaluate to the sets of worlds in which they hold. The distinction between global and local, deduction/entailment/completeness etc, is known in modal logic and also exists in ML. Roughly speaking, local deduction uses only the (logical) axioms and proof rules in the proof system of ML to prove patterns, while global deduction allows to prove patterns in theories, i.e., any sets of patterns that are taken as additional axioms, which can be used in the same way as the logical axioms. Similarly, local (semantic) entailment considers all models, while global entailment considers only models satisfying the given theory. In other words, local X is the special case of global X, where the underlying theory is the empty theory.
The two different completeness results are then stated as the following:
- Global completeness: global entailment implies global deduction, for all theories.
- Local completeness: local entailment implies local deduction.
Local completeness has been solved positively in the MmL paper, by a hard proof, inspired from local completeness proof of modal logic. Global completeness has been solved positively, for the case when the underlying theory contains the special definedness symbols, from which equality and membership can be defined as derived constructs.
The open problem is the the global completeness in its full generalarity, where the underlying theories may not contain definedness symbols.
OP2. Completeness and decidability of the quantifier-free fragment of MmL
Modal μ-logic is often called the "queen logic" for fixpoint reasoning, because of its rich expressiveness and good meta-properties. It has a (locally) complete proof system that can prove all valid formulas of the empty theory. Also, its SATISFIABILITY problem is decidable in the complexity class of EXPTIME-complete. Note that modal μ-logic is an extension of the basic modal logic with a binder μ that constructs least fixpoints, while MmL, excluding its FOL quantifiers, is an extension of the many-sorted polyadic modal logic with the binder μ. Therefore, we conjecture that the completeness and decidability of modal μ-logic can be generalized to the completeness and decidability of the quantifier-free fragment of MmL (QF-MmL), without FOL ∀/∃ quantifiers or element variables. Specifically, we conjecture that:
- QF-MmL has a (locally) complete proof system, given as the proof system of MmL, from which all axioms/rules about quantifiers are removed;
- The SATISFIABILITY of QF-MmL is decidable in EXPTIME.
Note that both the completeness and decidability of modal μ-logic are proved for the local case, as we discussed in OP1. We in further conjecture that the above two statements about QF-MmL also hold in the global sense for all theories.
OP3. Henkin semantics of MmL and its completeness
In the MmL paper, we capture precisely natural numbers with addition and multiplication in MmL, which shows that MmL cannot have a proof system that is both sound and complete. This drives us to look for an alternative semantics of MmL, where the least fixpoint patterns are not interpreted as the true least fixpoints in the models, but only the least fixpoints that are expressible in the logic. Such an alternative semantics is called Henkin Semantics, or General Semantics, in second-order logic or FOL with least fixpoints. Here, the open problem is to propose a similar Henkin semantics for MmL, and prove that the proof system we gave in the MmL paper is complete w.r.t. to the Henkin semantics.