Open Problems

From Matching Logic
Revision as of 04:59, 15 December 2019 by Xiaohong (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Here is a list of open problems and challenges about matching logic, in no particular order. In case you are interested in working on any of these problems, please contact us.

  1. Global completeness of fixpoint-free matching logic.
  2. We have shown in the following paper that the fixpoint-free fragment of matching logic has a sound and complete Hilbert-style proof system for the empty theory and any theories that contain a special set of symbols called definedness symbols, with which equalities and membership can be defined as syntactic sugar.

    Matching mu-Logic 
    Xiaohong Chen and Grigore Rosu
    LICS'19, ACM/IEEE, pp 1-13. 2019
    PDF, Slides(PPTX), Matching Logic, DOI, LICS'19, BIB

    However, it is open whether the proof system is complete for all theories, including those which are nonempty and do not contain the definedness symbols. This is known as the global completeness in literature because we care not just the empty theory (in which case it is called local completeness) but all theories.

    We used two different methods to prove the completeness for the empty theory and for theories with the definedness symbols. For the empty theory, we used a hybrid technology that combines the concept of witnesses in proving the completeness of FOL and the idea of canonical models in proving the completeness of modal logic. For theories with the definedness symbols, we defined a translation from fixpoint-free matching logic to FOL and reduced its completeness to the completeness of FOL. The translation is defined in the following paper

    Matching logic 
    Grigore Rosu
    LMCS, Volume 13(4), pp 1-61. 2017
    PDF, project, DOI, LMCS, BIB

    We need to prove the remaining cases, i.e., when the theories are not empty and do not contain the definedness symbols. For them, the reduction from matching logic completeness to FOL completeness no longer works because there is no way to re-produce the FOL proofs unless one has the definedness symbols (and thus equalities and membership). Therefore, we need to extend the hybrid technology that we used on the empty theory and to apply it to nonempty theories.

  3. Completeness and decidability of quantifier-free ML.
  4. Quantifier-free ML (abbreviated QFML) is the fragment of ML that contains no \exists-binders. QFML does contain the least fixpoint \mu-binder, so it is an extension of Modal mu-calculus. Modal mu-calculus is an important calculus for fixpoint reasoning because it is highly expressive and at the same time enjoys good meta-properties such as complete deduction and decidability of the SATISFIABILITY problem.

    We conjecture that QFML satisfies the same meta-properties. Specifically, we conjecture that

    • All valid QFML patterns can be proved by the proof system.
    • It is decidable to decide whether there exist a model and a valuation under which a given QFML pattern is interpreted to a nonempty set.
  5. Henkin semantics of ML.
  6. We have shown that there exists a theory in ML whose models are isomorphic to the standard model of natural numbers with addition and multiplication.

    Matching mu-Logic 
    Xiaohong Chen and Grigore Rosu
    LICS'19, ACM/IEEE, pp 1-13. 2019
    PDF, Slides(PPTX), Matching Logic, DOI, LICS'19, BIB

    This result implies, by Godel's first incompleteness system, that ML does not have an effective proof system that is both sound and complete for all theories.

    A similar situation exists in FOL with least fixpoints or in higher-order logic. In there, people investigate an alternative semantics called Henkin semantics or general semantics, where the least fixpoints are not interpreted as the true least fixpoints in the models, but only the least fixpoints that are expressible or definable by the syntax of the logics. And both logics become complete under Henkin semantic. Therefore, Henkin semantics offers a semantic viewpoint to the proof system and proof theories of FOL with least fixpoints and higher-order logic.

    We are looking for a Henkin semantics for ML. And It is not hard to define one. The challenge is to prove that the proposed semantics is complete with respect to the proof system of ML.

Personal tools