arXiv subjects

Minghui Ma

Publications and source records attributed to Minghui Ma.

27 records · Page 2Linked to original sources

arXiv2019

The Finite Model Property of Quasi-transitive Modal Logic

The finite model property of quasi-transitive modal logic $\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$ is established. This modal logic is conservatively extended to the tense logic $\mathsf{Kt}_2^3$. We present a Gentzen sequent calculus $\mathsf{G}$ for $\mathsf{Kt}_2^3$. The sequent calculus $\mathsf{G}$ has the finite algebra property by a finite syntactic construction. It follows that $\mathsf{Kt}_2^3$ and $\mathsf{K}_2^3$ have the finite model property.

cs.LO↗

arXiv2017

Graphical Sequent Calculi for Modal Logics

The syntax of modal graphs is defined in terms of the continuous cut and broken cut following Charles Peirce's notation in the gamma part of his graphical logic of existential graphs. Graphical calculi for normal modal logics are developed based on a reformulation of the graphical calculus for classical propositional logic. These graphical calculi are of the nature of deep inference. The relationship between graphical calculi and sequent calculi for modal logics is shown by translations between graphs and modal formulas.

cs.LO↗

arXiv2016

Sequent Calculi for Semi-De Morgan and De Morgan Algebras

A contraction-free and cut-free sequent calculus $\msf{G3SDM}$ for semi-De Morgan algebras, and a structural-rule-free and single-succedent sequent calculus $\msf{G3DM}$ for De Morgan algebras are developed. The cut rule is admissible in both sequent calculi. Both calculi enjoy the decidability and Craig interpolation. The sequent calculi are applied to prove some embedding theorems: $\msf{G3DM}$ is embedded into $\msf{G3SDM}$ via Gödel-Gentzen translation. $\msf{G3DM}$ is embedded into a sequent calculus for classical propositional logic. $\msf{G3SDM}$ is embedded into the sequent calculus $\msf{G3ip}$ for intuitionistic propositional logic.

math.LO↗

arXiv2016

Unified Correspondence and Proof Theory for Strict Implication

The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can be conservatively extended to Lambek Calculi over the bounded distributive full non-associative Lambek calculus (BDFNL). Many strict implication sequents can be transformed into analytic rules employing one of the main tools of unified correspondence theory, namely (a suitably modified version of) the Ackermann lemma based algorithm $\msf{ALBA}$. Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules which are transformed from strict implication sequents, are developed.

math.LO↗

arXiv2016

Unified Correspondence as a Proof-Theoretic Tool

The present paper aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into `analytic' structural rules of display calculi. In this context, a rule is `analytic' if adding it to a display calculus preserves Belnap's cut-elimination theorem. In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of nonclassical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices). We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics. The results of the present paper characterize the space of properly displayable DLE-logics.

math.LO↗

arXiv2015

Existence and bifurcation of solutions for a double coupled system of Schrodinger equations

Consider the following system of double coupled Schrödinger equations arising from Bose-Einstein condensates etc., \begin{equation*} \left\{\begin{array}{l} -Δu + u =μ_1 u^3 + βuv^2- κv, -Δv + v =μ_2 v^3 + βu^2v- κu, u\neq0, v\neq0\ \hbox{and}\ u, v\in H^1(\R^N), \end{array} \right. \end{equation*}where $μ_1, μ_2$ are positive and fixed, $κ$ and $β$ are linear and nonlinear coupling parameters respectively. We first use critical point theory and Liouville type theorem to prove some existence and nonexistence results on the positive solutions of this system. Then using the positive and non-degenerate solution of the scalar equation $-Δω+ω=ω^3$, $ω\in H_r^1(\R^N)$, we construct a synchronized solution branch to prove that for $β$ in certain range and fixed, there exist a series of bifurcations in product space $\R\times H^1_r(\R^N)\times H^1_r(\R^N)$ with parameter $κ$.

math.AP↗

arXiv2014

The Computational Compexity of Decision Problem in Additive Extensions of Nonassociative Lambek Calculus

We analyze the complexity of decision problems for Boolean Nonassociative Lambek Calculus admitting empty antecedent of sequents ($\mathsf{BFNL^*}$), and the consequence relation of Distributive Full Nonassociative Lambek Calculus ($\mathsf{DFNL}$). We construct a polynomial reduction from modal logic $\mathsf{K}$ into $\mathsf{BFNL^*}$. As a consequence, we prove that the decision problem for $\mathsf{BFNL^*}$ is PSPACE-hard. We also prove that the same result holds for the consequence relation of DFNL, by reducing $\mathsf{BFNL^*}$ in polynomial time to DFNL enriched with finite set of assumptions. Finally, we prove analogous results for variants of $\mathsf{BFNL^*}$, including $\mathsf{BFNL^*e}$ ($\mathsf{BFNL^*}$ with exchange), modal extensions of $\mathsf{BFNL^*_i}$ and $\mathsf{BFNL^*_{ei}}$ for $i \in \{\mathsf{K}, \mathsf{T}, \mathsf{K4}, \mathsf{S4}, \mathsf{S5}\}$.

cs.LO↗

arXiv2014

Residuated Basic Logic I

We study the residuated basic logic ($\mathsf{RBL}$) of residuated basic algebra in which the basic implication of Visser's basic propositional logic ($\mathsf{BPL}$) is interpreted as the right residual of a non-associative binary operator $\cdot$ (product). We develop an algebraic system $\mathsf{S_{RBL}}$ of residuated basic algebra by which we show that $\mathsf{RBL}$ is a conservative extension of $\mathsf{BPL}$. We present the sequent formalization $\mathsf{L_{RBL}}$ of $\mathsf{S_{RBL}}$ which is an extension of distributive full non-associative Lambek calculus ($\mathsf{DFNL}$), and show that the cut elimination and subformula property hold for it.

math.LO↗

arXiv2014

Residuated Basic Logic II. Interpolation, Decidability and Embedding

We prove that the sequent calculus $\mathsf{L_{RBL}}$ for residuated basic logic $\mathsf{RBL}$ has strong finite model property, and that intuitionistic logic can be embedded into basic propositional logic $\mathsf{BPL}$. Thus $\mathsf{RBL}$ is decidable. Moreover, it follows that the class of residuated basic algebras has the finite embeddability property, and that $\mathsf{BPL}$ is PSPACE-complete, and that intuitionistic logic can be embedded into the modal logic $\mathsf{K4}$.

math.LO↗