Interpreting Intuitionistic Propositional Logic in Terms of Intuitionistic Protothetics

An algebra of sentences of the quite intuitionistic protothetics, that is, an intuitionistic propositional logic with quantifiers augmented by the negation of the excluded middle, is a faithful model of intuitionistic propositional logic.     

Specialization of Loop Rules of a Sequent Calculus of Intuitionistic Temporal Logic with Time Gaps

The paper deals with the loop-rule problem in the first-order intuitionistic temporal logic sequent calculus LBJ. The calculus LBJT is intended for the specialization of the antecedent implication rule. The invertibility of some of the LBJT rules and the syntactic admissibility of the structural rules and the cut rule in LBJT, as well as the equivalence of LBJ and LBJT, are proved. The calculus LBJT2 is intended for the specialization of the antecedent universal quantifier and antecedent box rules. The decidability of LBJT2 is proved.     

Constants in Kripke Models for Intuitionistic Logic

We present a technique to extend a Kripke structure (for intuitionistic logic) into an elementary extension satisfying some property (cardinality, saturation, etc.) which can be “axiomatized” by a family of sets of sentences, where, most often, many constant symbols occur. To that end, we prove extended theorems of completeness and compactness. Also, a section of the paper is devoted to the back-and-forth construction of isomorphisms between Kripke structures.     

Infinitary Calculus without Loop Rules for Restricted Sequents of the First-Order Linear Temporal Logic

A restricted first-order linear temporal logic with temporal operators next and always is considered. We prove that for this logic one can construct a sequential calculus without loop rules, i.e., the rules containing a duplication of the main formula in the premises of these rules. This paper continues the previous work of the author, where an infinitary calculus without loop rules on the logical level, but containing the traditional loop antecedent rule for the operator always, was constructed. In this paper, in order to remove this loop rule we introduce a nonlocal rule allowing us to eliminate loops in the process of the proof search. The soundness and >-completeness of the constructed calculus is proved.     

Categorical Abstract Algebraic Logic: Algebraizable Institutions

The framework developed by Blok and Pigozzi for the algebraizability of deductive systems is extended to cover the algebraizability of multisignature logics with quantifiers. Institutions are used as the supporting structure in place of deductive systems. In particular, the concept of an algebraic institution and that of an algebraizable institution are made precise using the theory of monads from categorical algebra and the notion of equivalence of institutions introduced by Voutsadakis. Several examples of algebraic and algebraizable institutions are provided.     

A secondary semantics for Second Order Intuitionistic Propositional Logic

In this paper we propose a Kripke‐style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

THE JUDGEMENT CALCULUS FOR INTUITIONISTIC LINEAR LOGIC: PROOF THEORY AND SEMANTICS

In this paper we propose a new set of rules for a judgement calculus, i.e. a typed lambda calculus, based on Intuitionistic Linear Logic; these rules ease the problem of defining a suitable mathematical semantics. A proof of the canonical form theorem for this new system is given: it assures, beside the consistency of the calculus, the termination of the evaluation process of every well-typed element. The definition of the mathematical semantics and a completeness theorem, that turns out to be a representation theorem, follow. This semantics is the basis to obtain a semantics for the evaluation process of every well-typed program. 1991 MSC: 03B20, 03B40.     

A Decision Procedure for Nonperiodic Sequents of the First-Order Linear Temporal Logic

A deduction-based decision procedure is presented for the nonperiodic D-sequents of the first-order linear temporal logic. The D-sequents are obtained from D ₂-sequents [7], [8] by removing the periodicity condition. The deductive procedure proposed consists of decidable deductive procedures that replace infinitary and finitary induction rules for the temporal operator ``always'. The soundness and completeness of the deduction-based decision procedure proposed is proved.     

一类直觉模糊关系线性规划的解

提出了一类目标函数为线性函数,约束是直觉模糊关系方程的最优化问题.这是一类非凸非光滑最优化问题,基于可行域的结构,给出了求全局最优解和最优值的一个算法,最后通过数值例子验证了算法的可行性.     

直觉主义量词模态逻辑系统MIPC~*的可靠性定理

设WMμ为系统MIPC*全部公式的集,再设г∪{A} WMμ,则гMIPC* A意义明显.而 M A指гM-蕴涵A.以前已证明гM A гMIPC*A,即MIPC*为强完全的.本文证明其逆定理成立,即гMIPC*A гM A.是为MIPC*的可靠性定理.     

线性逻辑和态极逻辑引论(Ⅰ)

《线性逻辑和态极逻辑引论》一文概述了由Girard分别于1986和2001所创建的线性逻辑和态极逻辑.线性逻辑和态极逻辑汲取于计算机科学并反之应用于其中,从根本上对数理逻辑进行了彻底的审视.全文分为两部分.本文是文章的第一部分,致力于线性逻辑的联结词、证明规则、可判定性性质和模型.文章的第二部分将研究证明网并简要介绍态极逻辑.证明网是证明的图式表示,是线性逻辑的主要创新之一.     

The Brauer-Clifford group for locally finite (S,H)-Azumaya algebras

In this article, we define the notion of Brauer-Clifford group for H-locally finite (S, H)-Azumaya algebras, when H is a cocommutative Hopf algebra and S is an H-locally finite commutative H-module algebra over a commutative noetherian ring k. This is the situation that arises in applications with connections to algebraic geometry. This Brauer-Clifford group turns out to be an example of a Brauer group of a symmetric monoidal category.     

线性逻辑和态极逻辑引论(Ⅱ)

本文是《线性逻辑和态极逻辑引论》一文的第二部分。文章致力于证明网(第1节)和态极逻辑(第2,3,4和5节)证明网部分尽管局限于其积线性逻辑框架,但仍不失其重要性。线性逻辑和态极逻辑均为Girard所创建,近期所发展起来的态极逻辑旨在于进一步揭示计算和逻辑的基本交互作用的本质。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。     

Strong Normalizability of Typed Lambda-Calculi for Substructural Logics

The strong normalization theorem is uniformly proved for typed λ-calculi for a wide range of substructural logics with or without strong negation. We would like to thank the referees for their valuable comments and suggestions. This research was supported by the Alexander von Humboldt Foundation. The second author is grateful to the Foundation for providing excellent working conditions and generous support of this research. This work was also supported by the Japanese Ministry of Education, Culture, Sports, Science and Technology, Grant-in-Aid for Young Scientists (B) 20700015, 2008.     

直觉模糊多属性的意见集中排序法

研究了属性权重信息不完全确定,属性值为直觉模糊集的多属性决策问题。首先根据直觉模糊数的得分函数和精确函数对决策矩阵中的评价值比较大小,进而按属性集中的每个属性对方案排成线性序;然后通过计算赋权模糊优先矩阵确定方案的优属度,建立规划模型确定属性的权重;再利用加权算术算子对方案集结,得到专家对方案的排序,从而得到一种新的意见集中排序的决策方法。数值实例说明该方法的有效性和实用性,可为解决直觉模糊多属性决策提供新方法     

Glivenko Classes of Sequents for Temporal Logic with Time Gaps

Let LB be a sequent calculus of the first-order classical temporal logic TB with time gaps. Let, further, LBJ be the intuitionistic counterpart of LB. In this paper, we consider conditions under which a sequent is derivable in the calculus LBJ if and only if it is derivable in the calculus LB. Such conditions are defined for sequents with one formula in the succedent (purely Glivenko -classes) and for sequents with the empty succedent (Glivenko -classes).     

Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas

An infinitary calculus for a restricted fragment of the first-order linear temporal logic is considered. We prove that for this fragment one can construct the infinitary calculusG _Lω ^* without contraction on predicate formulas. The calculusG _Lω ^* possesses the following properties: (1) the succedent rule for the existential quantifier is included into the corresponding axiom; (2) the premise of the antecedent rule for the universal quantifier does not contain a duplicate of the main formula. The soundness and completness ofG _Lω ^* are also proved. Institute of Mathematics and Informatics, Akademijos 4, 2600 Vilnius, Lithuania. Translated from Lietuvos Matematikos Rinkinys, Vol. 39, No. 3, pp. 378–397, July–September, 1999. Translated by R. Lapinskas     

A Basis in Semi‐Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC

We study the problem of finding a basis for all rules admissible in the intuitionistic propositional logic IPC. The main result is Theorem 3.1 which gives a basis consisting of all rules in semi‐reduced form satisfying certain specific additional requirements. Using developed technique we also find a basis for rules admissible in the logic of excluded middle law KC.     

A Sequent Calculus for Propositional Dynamic Logic for Agents

We consider propositional dynamic logic for agents. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.     

求解病态线性方程组的收缩Lanczos方法

Lanczos方法是求解大型线性方程组的常用方法.遗憾的是,在Lanczos过程中通常会发生算法中断或数值不稳定的情况.将给出求解大型对称线性方程组的收缩Lanczos方法,即DLanczos方法.新算法将采用增广子空间技术,在Lanczos过程中向Krylov子空间加入少量绝对值较小的特征值所对应的特征向量进行收缩.数值实验表明,新算法比Lanczos方法收敛速度更快,并且适合求解病态对称线性方程组.