Sequent Calculi for Some Strict Implication Logics

We introduce various sequent systems for propositional logicshaving strict implication, and prove the completeness theoremsand the finite model properties of these systems.The cut-eliminationtheorems or the (modified) subformula properties are provedsemantically.     

Sequent Calculi and Decision Procedures for Weak Modal Systems

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb rules are given.     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.     

Proof Systems Combining Classical and Paraconsistent Negations

New propositional and first-order paraconsistent logics (called L _ω and FL _ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L _ω and FL _ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L _ω and FL _ω are proved. The cut-elimination theorems for L _ω and FL _ω are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems. Presented by Yaroslav Shramko and Heinrich Wansing     

An O(n log n)-Space Decision Procedure for the Relevance Logic B+

In previous work we gave a new proof-theoretical method for establishing upper-bounds on the space complexity of the provability problem of modal and other propositional non-classical logics. Here we extend and refine these results to give an O(n log n)-space decision procedure for the basic positive relevance logic B⁺. We compute this upper-bound by first giving a sound and complete, cut-free, labelled sequent system for B⁺, and then establishing bounds on the application of the rules of this system.     

Labeled Calculi and Finite-Valued Logics

A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite-valued logic if the labels are interpreted as sets of truth values (sets-as-signs). Furthermore, it is shown that any finite-valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the number of truth values, and it is shown that this bound is tight.     

Uniform Interpolation and Propositional Quantifiers in Modal Logics

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible. We shall present such a proof of the uniform interpolation theorem for normal modal logics K and T. It provides an explicit algorithm constructing the interpolants. Presented by Heinrich Wansing     

Harmonising natural deduction

Prawitz proved a theorem, formalising ‘harmony’ in Natural Deduction systems, which showed that, corresponding to any deduction there is one to the same effect but in which no formula occurrence is both the consequence of an application of an introduction rule and major premise of an application of the related elimination rule. As Gentzen ordered the rules, certain rules in Classical Logic had to be excepted, but if we see the appropriate rules instead as rules for Contradiction, then we can extend the theorem to the classical case. Properly arranged there is a thoroughgoing ‘harmony’, in the classical rules. Indeed, as we shall see, they are, all together, far more ‘harmonious’ in the general sense than has been commonly observed. As this paper will show, the appearance of disharmony has only arisen because of the illogical way in which natural deduction rules for Classical Logic have been presented.     

后腹腔镜肾盂输尿管切开取石术34例临床体会

探讨后腹腔镜下肾孟、输尿管切开取石的技术要点和临床应用价值。回顾性分析34例后腹腔镜肾盂、输尿管切开取石术的临床质料。男22例,女12例,肾盂结石10例,输尿管结石24例。结果34例成功完成腹腔镜取石术,手术时间40min～90min,平均58min,术中出血10ml～30ml,术后1例漏尿3d,术后3d～5d拔除后腹...     

Gentzen-Type Methods for Bilattice Negation

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLS_cw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLS_cw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL.