Results for 'cut rule'

973 found
Order:
  1.  93
    (1 other version)Cut-rule axiomatization of the syntactic calculus NL.Wojciech Zielonka - 2000 - Journal of Logic, Language and Information 9 (3):339-352.
    An axiomatics of the product-free syntactic calculus L ofLambek has been presented whose only rule is the cut rule. It was alsoproved that there is no finite axiomatics of that kind. The proofs weresubsequently simplified. Analogous results for the nonassociativevariant NL of L were obtained by Kandulski. InLambek's original version of the calculus, sequent antecedents arerequired to be nonempty. By removing this restriction, we obtain theextensions L 0 and NL 0 ofL and NL, respectively. Later, the finiteaxiomatization problem (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  2.  9
    Cut-Rule Axiomatization of the Syntactic Calculus L0.Wojciech Zielonka - 2001 - Journal of Logic, Language and Information 10 (2):233-236.
    In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L0 of L. This modification, introduced in the early 1980s (see, e.g., (...)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  21
    (1 other version)Cut‐Rule Axiomatization of Product‐Free Lambek Calculus With the Empty String.Wojciech Zielonka - 1988 - Mathematical Logic Quarterly 34 (2):135-142.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  4. Gentzen’s “cut rule” and quantum measurement in terms of Hilbert arithmetic. Metaphor and understanding modeled formally.Vasil Penchev - 2022 - Logic and Philosophy of Mathematics eJournal 14 (14):1-37.
    Hilbert arithmetic in a wide sense, including Hilbert arithmetic in a narrow sense consisting by two dual and anti-isometric Peano arithmetics, on the one hand, and the qubit Hilbert space (originating for the standard separable complex Hilbert space of quantum mechanics), on the other hand, allows for an arithmetic version of Gentzen’s cut elimination and quantum measurement to be described uniformy as two processes occurring accordingly in those two branches. A philosophical reflection also justifying that unity by quantum neo-Pythagoreanism links (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  5.  60
    Protoalgebraic Gentzen systems and the cut rule.Àngel J. Gil & Jordi Rebagliato - 2000 - Studia Logica 65 (1):53-89.
    In this paper we show that, in Gentzen systems, there is a close relation between two of the main characters in algebraic logic and proof theory respectively: protoalgebraicity and the cut rule. We give certain conditions under which a Gentzen system is protoalgebraic if and only if it possesses the cut rule. To obtain this equivalence, we limit our discussion to what we call regular sequent calculi, which are those comprising some of the structural rules and some logical (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  6.  39
    Disjunctive logic programs, answer sets, and the cut rule.Éric Martin - 2022 - Archive for Mathematical Logic 61 (7):903-937.
    In Minker and Rajasekar (J Log Program 9(1):45–74, 1990), Minker proposed a semantics for negation-free disjunctive logic programs that offers a natural generalisation of the fixed point semantics for definite logic programs. We show that this semantics can be further generalised for disjunctive logic programs with classical negation, in a constructive modal-theoretic framework where rules are built from _claims_ and _hypotheses_, namely, formulas of the form φ\Box \varphi and φ\Diamond \Box \varphi where φ\varphi is a literal, respectively, (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  7.  64
    Cut elimination for a calculus with context-dependent rules.Birgit Elbl - 2001 - Archive for Mathematical Logic 40 (3):167-188.
    Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8. On cut elimination in the presence of perice rule.Lev Gordeev - 1987 - Archive for Mathematical Logic 26 (1):147-164.
     
    Export citation  
     
    Bookmark   6 citations  
  9.  46
    Which Structural Rules Admit Cut Elimination? An Algebraic Criterion.Kazushige Terui - 2007 - Journal of Symbolic Logic 72 (3):738 - 754.
    Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  10.  73
    Normal Proofs, Cut Free Derivations and Structural Rules.Greg Restall - 2014 - Studia Logica 102 (6):1143-1166.
    Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which differs again (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  11.  17
    Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
    We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the K\mathsf{K}, D\mathsf{D}, T\mathsf{T}, K4\mathsf{K4}, D4\mathsf{D4} and S4\mathsf{S4} spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \Box and \Diamond. Starting points for this research are 2-sequents and indexed-based (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  12.  15
    5.'Cut-and-paste'? Rule of law promotion and legal transplants in war to peace transitions.Richard Zajac Sannerholm - 2009 - In Antonina Bakardjieva Engelbrekt (ed.), New Directions in Comparative Law. Edward Elgar.
    Direct download  
     
    Export citation  
     
    Bookmark  
  13.  40
    Cut Elimination for GLS Using the Terminability of its Regress Process.Jude Brighton - 2016 - Journal of Philosophical Logic 45 (2):147-153.
    The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  14. (1 other version)A Cut-Free Sequent Calculus for Defeasible Erotetic Inferences.Jared Millson - 2019 - Studia Logica (6):1-34.
    In recent years, the e ffort to formalize erotetic inferences (i.e., inferences to and from questions) has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and regular erotetic implication. While an attempt has been made to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  15. Cut for core logic.Neil Tennant - 2012 - Review of Symbolic Logic 5 (3):450-479.
    The motivation for Core Logic is explained. Its system of proof is set out. It is then shown that, although the system has no Cut rule, its relation of deducibility obeys Cut with epistemic gain.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   25 citations  
  16.  52
    Rasiowa–Sikorski Deduction Systems with the Rule of Cut: A Case Study.Dorota Leszczyńska-Jasion, Mateusz Ignaszak & Szymon Chlebowski - 2019 - Studia Logica 107 (2):313-349.
    This paper presents Rasiowa–Sikorski deduction systems for logics \, \, \ and \. For each of the logics two systems are developed: an R–S system that can be supplemented with admissible cut rule, and a \-version of R–S system in which the non-admissible rule of cut is the only branching rule. The systems are presented in a Smullyan-like uniform notation, extended and adjusted to the aims of this paper. Completeness is proved by the use of abstract refutability (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  17.  93
    Cut and pay.Marcelo Finger & Dov Gabbay - 2006 - Journal of Logic, Language and Information 15 (3):195-218.
    In this paper we study families of resource aware logics that explore resource restriction on rules; in particular, we study the use of controlled cut-rule and introduce three families of parameterised logics that arise from different ways of controlling the use of cut. We start with a formulation of classical logic in which cut is non-eliminable and then impose restrictions on the use of cut. Three Cut-and-Pay families of logics are presented, and it is shown that each family provides (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  18.  77
    Cut-free tableau calculi for some propositional normal modal logics.Martin Amerbauer - 1996 - Studia Logica 57 (2-3):359 - 372.
    We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G 0(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G 0are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  19.  45
    A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
    In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  20. A cut-free sequent calculus for the bi-intuitionistic logic 2Int.Sara Ayhan - manuscript
    The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist reasoning, since they (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  43
    Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi.Richard Zach - 2021 - Review of Symbolic Logic 14 (3):645-686.
    Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot’s free deduction. The elimination rules are “general,” but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  22.  62
    “Cuts in Action”: A High‐Density EEG Study Investigating the Neural Correlates of Different Editing Techniques in Film.Katrin S. Heimann, Sebo Uithol, Marta Calbi, Maria A. Umiltà, Michele Guerra & Vittorio Gallese - 2017 - Cognitive Science 41 (6):1555-1588.
    In spite of their striking differences with real-life perception, films are perceived and understood without effort. Cognitive film theory attributes this to the system of continuity editing, a system of editing guidelines outlining the effect of different cuts and edits on spectators. A major principle in this framework is the 180° rule, a rule recommendation that, to avoid spectators’ attention to the editing, two edited shots of the same event or action should not be filmed from angles differing (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  23.  32
    Cut-Elimination: Syntax and Semantics.M. Baaz & A. Leitsch - 2014 - Studia Logica 102 (6):1217-1244.
    In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the generalized (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24. Capturing naive validity in the Cut-free approach.Eduardo Barrio, Lucas Rosenblatt & Diego Tajer - 2016 - Synthese 199 (Suppl 3):707-723.
    Rejecting the Cut rule has been proposed as a strategy to avoid both the usual semantic paradoxes and the so-called v-Curry paradox. In this paper we consider if a Cut-free theory is capable of accurately representing its own notion of validity. We claim that the standard rules governing the validity predicate are too weak for this purpose and we show that although it is possible to strengthen these rules, the most obvious way of doing so brings with it a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  25. Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
    A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   53 citations  
  26.  13
    Axioms vs. rewrite rules: From completeness to cut elimination.Gilles Dowek - 2000 - In Dov M. Gabbay & Maarten de Rijke (eds.), Frontiers of combining systems 2. Philadelphia, PA: Research Studies Press. pp. 62--72.
  27.  44
    Cut‐Elimination Theorem for the Logic of Constant Domains.Ryo Kashima & Tatsuya Shimura - 1994 - Mathematical Logic Quarterly 40 (2):153-172.
    The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...)
    Direct download  
     
    Export citation  
     
    Bookmark   6 citations  
  28. A cut-free sequent system for two-dimensional modal logic, and why it matters.Greg Restall - 2012 - Annals of Pure and Applied Logic 163 (11):1611-1623.
    The two-dimensional modal logic of Davies and Humberstone [3] is an important aid to our understanding the relationship between actuality, necessity and a priori knowability. I show how a cut-free hypersequent calculus for 2D modal logic not only captures the logic precisely, but may be used to address issues in the epistemology and metaphysics of our modal concepts. I will explain how the use of our concepts motivates the inference rules of the sequent calculus, and then show that the completeness (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   27 citations  
  29. Cuts and clouds: vagueness, its nature, and its logic.Richard Dietz & Sebastiano Moruzzi (eds.) - 2010 - New York: Oxford University Press.
    Vagueness is a familiar but deeply puzzling aspect of the relation between language and the world. It is highly controversial what the nature of vagueness is -- a feature of the way we represent reality in language, or rather a feature of reality itself? May even relations like identity or parthood be affected by vagueness? Sorites arguments suggest that vague terms are either inconsistent or have a sharp boundary. The account we give of such paradoxes plays a pivotal role for (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  30.  4
    Uniform Cut-Free Bisequent Calculi for Three-Valued Logics.Andrzej Indrzejczak & Yaroslav Petrukhin - 2024 - Logic and Logical Philosophy 33 (3):463-506.
    We present a uniform characterisation of three-valued logics by means of a bisequent calculus (BSC). It is a generalised form of a sequent calculus (SC) where rules operate on the ordered pairs of ordinary sequents. BSC may be treated as the weakest kind of system in the rich family of generalised SC operating on items being some collections of ordinary sequents, like hypersequent and nested sequent calculi. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  31.  53
    Cut elimination and strong separation for substructural logics: an algebraic approach.Nikolaos Galatos & Hiroakira Ono - 2010 - Annals of Pure and Applied Logic 161 (9):1097-1133.
    We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  32.  57
    Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics.Adam Přenosil - 2017 - Studia Logica 105 (6):1255-1289.
    We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  33.  31
    Cut and gamma I: Propositional and constant domain R.Yale Weiss - 2020 - Review of Symbolic Logic 13 (4):887-909.
    The main object of this article is to give two novel proofs of the admissibility of Ackermann’s rule (γ) for the propositional relevant logic R. The results are established as corollaries of cut elimination for systems of tableaux for R. Cut elimination, in turn, is established both nonconstructively (as a corollary of completeness) and constructively (using Gentzen-like methods). The extensibility of the techniques is demonstrated by showing that (γ) is admissible for RQ* (R with constant domain quantifiers). The status (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34.  54
    Syntactic cut-elimination for common knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.
    We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to give (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  35.  26
    Cut elimination for coherent theories in negation normal form.Paolo Maffezioli - 2024 - Archive for Mathematical Logic 63 (3):427-445.
    We present a cut-free sequent calculus for a class of first-order theories in negation normal form which include coherent and co-coherent theories alike. All structural rules, including cut, are admissible.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  36.  86
    Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D.Samara Burns & Richard Zach - 2021 - Review of Symbolic Logic 14 (4):910-929.
    We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37. Cut-free single-pass tableaux for the logic of common knowledge.Rajeev Gore - unknown
    We present a cut-free tableau calculus with histories and variables for the EXPTIME-complete multi-modal logic of common knowledge. Our calculus constructs the tableau using only one pass, so proof-search for testing theoremhood of ϕ does not exhibit the worst-case EXPTIME-behaviour for all ϕ as in two-pass methods. Our calculus also does not contain a “finitized ω-rule” so that it detects cyclic branches as soon as they arise rather than by worst-case exponential branching with respect to the size of ϕ. (...)
     
    Export citation  
     
    Bookmark  
  38.  21
    Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs.Marcelo Finger & Dov Gabbay - 2007 - Logic Journal of the IGPL 15 (5-6):553-575.
    This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof. We then concentrate on the problem of efficiently computing non-analytic cuts. (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  39.  17
    A reduction-based cut-free Gentzen calculus for dynamic epistemic logic1.Martin Wirsing & Alexander Knapp - 2023 - Logic Journal of the IGPL 31 (6):1047-1068.
    Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  40. Cut elimination for systems of transparent truth with restricted initial sequents.Carlo Nicolai - manuscript
    The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  41. Cut Elimination inside a Deep Inference System for Classical Predicate Logic.Kai Brünnler - 2006 - Studia Logica 82 (1):51-71.
    Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  42. Cut-Elimination and Quantification in Canonical Systems.Anna Zamansky & Arnon Avron - 2006 - Studia Logica 82 (1):157-176.
    Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  43. Analytic cut trees.Carlo Cellucci - 2000 - Logic Journal of the IGPL 8 (6):733-750.
    It has been maintained by Smullyan that the importance of cut-free proofs does not stem from cut elimination per se but rather from the fact that they satisfy the subformula property. In accordance with such a viewpoint in this paper we introduce analytic cut trees, a system from which cuts cannot be eliminated but satisfying the subformula property. Like tableaux analytic cut trees are a refutation system but unlike tableaux they have a single inference rule and several branch closure (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  44. Formalised cut admissibility for display logic.Rajeev Gore - manuscript
    We use a deep embedding of the display calculus for relation algebras RA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for RA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.
     
    Export citation  
     
    Bookmark  
  45. Strong Cut-Elimination, Coherence, and Non-deterministic Semantics.Arnon Avron - unknown
    An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...)
     
    Export citation  
     
    Bookmark  
  46. Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown
    We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle /HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle /HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.
     
    Export citation  
     
    Bookmark  
  47.  55
    Cut-free tableau calculi for some intuitionistic modal logics.Mauro Ferrari - 1997 - Studia Logica 59 (3):303-330.
    In this paper we provide cut-free tableau calculi for the intuitionistic modal logics IK, ID, IT, i.e. the intuitionistic analogues of the classical modal systems K, D and T. Further, we analyse the necessity of duplicating formulas to which rules are applied. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Specifically, we enlarge the language with the new signs Fc and CR near to the usual (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  48.  57
    Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions.Heine Sørensen Morten & Urzyczyn Paweł - 2008 - Journal of Symbolic Logic 73 (3):919-932.
    There is a simple technique, due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop’s ι-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings; it is (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  49.  76
    Cut Elimination for S4C: A Case Study.Grigori Mints - 2006 - Studia Logica 82 (1):121-132.
    S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  50.  29
    A new technique for proving realisability and consistency theorems using finite paraconsistent models of cut‐free logic.Arief Daynes - 2006 - Mathematical Logic Quarterly 52 (6):540-554.
    A new technique for proving realisability results is presented, and is illustrated in detail for the simple case of arithmetic minus induction. CL is a Gentzen formulation of classical logic. CPQ is CL minus the Cut Rule. The basic proof theory and model theory of CPQ and CL is developed. For the semantics presented CPQ is a paraconsistent logic, i.e. there are non-trivial CPQ models in which some sentences are both true and false. Two systems of arithmetic minus induction (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 973