Switch to: References

Add citations

You must login to add citations.
  1. 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 \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\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 calculi (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • On Reduction Rules, Meaning-as-Use, and Proof-Theoretic Semantics.Ruy J. G. B. de Queiroz - 2008 - Studia Logica 90 (2):211 - 247.
    The intention here is that of giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett-Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i. e. the so-called reduction rules. For that we suggest an (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • The placeholder view of assumptions and the Curry–Howard correspondence.Ivo Pezlar - 2020 - Synthese (11):1-17.
    Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • 1995 European Summer Meeting of the Association for Symbolic Logic.Johann A. Makowsky - 1997 - Bulletin of Symbolic Logic 3 (1):73-147.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • From Tractatus to Later Writings and Back – New Implications from Wittgenstein’s Nachlass.Ruy J. G. B. de Queiroz - 2023 - SATS 24 (2):167-203.
    As a celebration of theTractatus100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that “everyone is aware of the holistic character of Wittgenstein’s later philosophy, but it is not so well known that it was already beginning to establish itself in theTractatus” (The False Prison, 1987). From the latter to the former, Stephen Hilmy’s (The Later Wittgenstein, 1987) extensive study of theNachlasshas helped removing classical misconceptions such as (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • On reduction rules, meaning-as-use, and proof-theoretic semantics.Ruy J. G. B. de Queiroz - 2008 - Studia Logica 90 (2):211-247.
    The intention here is that of giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett–Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i.e. the so-called reduction rules. For that we suggest an extension (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Proof-finding Algorithms for Classical and Subclassical Propositional Logics.M. W. Bunder & R. M. Rizkalla - 2009 - Notre Dame Journal of Formal Logic 50 (3):261-273.
    The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in Dekker. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Modal pure type systems.Tijn Borghuis - 1998 - Journal of Logic, Language and Information 7 (3):265-296.
    We present a framework for intensional reasoning in typed -calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a propositions-as-types-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • A proof-theoretic investigation of a logic of positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.
    We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations