Modal logic as metalogic

The goal of this paper is to show how modal logic may be conceived as recording the derived rules of a logical system in the system itself. This conception of modal logic was propounded by Dana Scott in the early seventies. Here, similar ideas are pursued in a context less classical than Scott's.First a family of propositional logical systems is considered, which is obtained by gradually adding structural rules to a variant of the nonassociative Lambek calculus. In this family one finds systems that correspond to the associative Lambek calculus, linear logic, relevant logics, BCK logic and intuitionistic logic. Above these basic systems, sequent systems parallel to the basic systems are constructed, which formalize various notions of derived rules for the basic systems. The deduction theorem is provable for the basic systems if, and only if, they are at least as strong as systems corresponding to linear logic, or BCK logic, depending on the language, and their deductive metalogic is not stronger than they are.However, though we do not always have the deduction theorem, we may always obtain a modal analogue of the deduction theorem for conservative modal extensions of the basic systems. Modal postulates which are necessary and sufficient for that are postulates of S4 plus modal postulates which mimic structural rules. For example, the modal postulates which Girard has recently considered in linear logic are necessary and sufficient for the modal analogue of the deduction theorem.All this may lead towards results about functional completeness in categories. When functional completeness, which is analogous to the deduction theorem, fails, we may perhaps envisage a modal analogue of functional completeness in a modal category, of which our original category is a full subcategory.     

Decidability by Resolution for Propositional Modal Logics

The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalization, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimized functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, many standard first-order theorem provers that are based on resolution are suitable for facilitating modal reasoning.     

Substructural Logics with Mingle

We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FL_m (full Lambek logic with the mingle), GL_m(Girard's linear logic with the mingle) and L_m (Lambek calculuswith restricted mingle).     

SAT-Based Decision Procedures for Classical Modal Logics

We present a set of SAT-based decision procedures for various classical modal logics. By SAT based, we mean built on top of a SAT solver. We show how the SAT-based approach allows for a modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation. For the others, we define a testing methodology that generalizes the 3CNF _K methodology by Giunchiglia and Sebastiani. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures.     

Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the “next” temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time analysis via the Curry-Howard isomorphism. However, he did not investigate the logic itself in detail; he has proved only that the logic augmented with negation and classical reasoning is equivalent to (the “next” fragment of) the standard formulation of classical linear-time temporal logic. We give natural deduction, sequent calculus and Hilbert-style proof systems for constructive LTL with conjunction, disjunction and falsehood, and show that the sequent calculus enjoys cut elimination. Moreover, we also consider Kripke semantics and prove soundness and completeness. One distinguishing feature of this logic is that distributivity of the “next” operator over disjunction “?(A∨B)⊃?A∨?B” is rejected in view of a type-theoretic interpretation.     

Labelled Modal Logics: Quantifiers

In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4.2, KD45, and S5. Here we extend this approach to quantified modal logics, providing formalizations for logics with varying, increasing, decreasing, or constant domains. The result is modular with respect to both properties of the accessibility relation in the Kripke frame and the way domains of individuals change between worlds. Our approach has a modular metatheory too; soundness, completeness and normalization are proved uniformly for every logic in our class. Finally, our work leads to a simple implementation of a modal logic theorem prover in a standard logical framework.     

公式分层的谓词模态逻辑

由于必然模态词□的引入,谓词模态逻辑的公式在一个可能世界中的真假值可能依赖于其可达的可能世界.在谓词模态逻辑中存在个体跨可能世界相等问题.针对这一问题,Lewis提出了对应物理论,并且在对应物理论中用对应物关系来表示个体跨可能世界相等.但是,当一个对象具有一个以上的对应物时,谓词模态逻辑中的跨可能世界相等关系无法与对应物关系建立一一对应.通过限制谓词模态逻辑中全称量词∀的范围,给出了一种公式分层的谓词模态逻辑.它是谓词模态逻辑的一个子逻辑,并且其语言与谓词模态逻辑的语言是相同的.但其公式是分层定义的,使得∀可以出现在□的范围内,并且□不能出现在∀的范围内.由于任意形如∀x□φ（x）的表达式都不是该逻辑的公式,以量词开头的公式在一个可能世界w中的真假值只依赖于w,该逻辑避免了个体跨可能世界相等问题.给出了该逻辑的语言、语法和语义,并证明了该逻辑是可靠的和完备的.     

概率信念逻辑的语义

在信念逻辑基础上,引入概率,给出了一种概率信念逻辑PBL,增强了信念逻辑的表述能力和推理能力。并为PBL建立了两种语义：首先将知识逻辑的Aumann语义进行推广,给出了PBL逻辑的概率Aumann语义,其次为PBL建立了一种正规概率模态语义,这是一种适于刻画概率模态逻辑的语义模型。证明了PBL的概率Aumann语义和正规概率模记语义的可靠性,并讨论了正规概率模态语义与Kripke语义的关系。最后,通过一个例子说明了PBL的描述能力和推理能力。