Switch to: References

Add citations

You must login to add citations.
  1. Uniform interpolation in substructural logics.Majid Alizadeh, Farzaneh Derakhshan & Hiroakira Ono - 2014 - Review of Symbolic Logic 7 (3):455-483.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • 1998 European Summer Meeting of the Association for Symbolic Logic.S. Buss - 1999 - Bulletin of Symbolic Logic 5 (1):59-153.
    Download  
     
    Export citation  
     
    Bookmark  
  • Kripke semantics and proof systems for combining intuitionistic logic and classical logic.Chuck Liang & Dale Miller - 2013 - Annals of Pure and Applied Logic 164 (2):86-111.
    We combine intuitionistic logic and classical logic into a new, first-order logic called polarized intuitionistic logic. This logic is based on a distinction between two dual polarities which we call red and green to distinguish them from other forms of polarization. The meaning of these polarities is defined model-theoretically by a Kripke-style semantics for the logic. Two proof systems are also formulated. The first system extends Gentzenʼs intuitionistic sequent calculus LJ. In addition, this system also bears essential similarities to Girardʼs (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Scrutinizing Anti-exceptionalism. Mansooreh - manuscript
    In this paper, I argue against present accounts of anti-exceptionalism about logic, while preserving some of their insights. I will do that by offering objections against the anti-exceptionalists’ claims that revisions happen in the same way in sciences and in logic, and that the methodology of logic involves abduction simpliciter. I propose a new account of theory divergence for logic with anti-exceptionalist aspects which also preserves exceptionalism on some level while considering the role of metalogic in the exceptionalist/anti-exceptionalist debate.
    Download  
     
    Export citation  
     
    Bookmark  
  • On an interpretation of second order quantification in first order intuitionistic propositional logic.Andrew M. Pitts - 1992 - Journal of Symbolic Logic 57 (1):33-52.
    We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...)
    Download  
     
    Export citation  
     
    Bookmark   49 citations  
  • Topics in the Proof Theory of Non-classical Logics. Philosophy and Applications.Fabio De Martin Polo - 2023 - Dissertation, Ruhr-Universität Bochum
    Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them in two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice of working with (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Loop-Check Specification for a Sequent Calculus of Temporal Logic.Romas Alonderis, Regimantas Pliuškevičius, Aida Pliuškevičienė & Haroldas Giedra - 2022 - Studia Logica 110 (6):1507-1536.
    In our previous work we have introduced loop-type sequent calculi for propositional linear discrete tense logic and proved that these calculi are sound and complete. Decision procedures using the calculi have been constructed for the considered logic. In the present paper we restrict ourselves to the logic with the unary temporal operators “next” and “henceforth always”. Proof-theory of the sequent calculus of this logic is considered, focusing on loop specification in backward proof-search. We describe cyclic sequents and prove that any (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • The G4i Analogue of a G3i Sequent Calculus.Rosalie Iemhoff - 2022 - Studia Logica 110 (6):1493-1506.
    This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic L with a cut-free calculus G that is an extension of G3ip the method produces a terminating analytic calculus that is an extension of G4ip and equivalent to G. G4ip was introduced by Roy Dyckhoff in 1992 as a terminating analogue of the calculus G3ip for intuitionistic propositional logic. Thus this paper can be viewed as an extension of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Logic, Language, Information and Computation: 15th International Workshop, Wollic 2008 Edinburgh, Uk, July 1-4, 2008, Proceedings.Wilfrid Hodges & Ruy de Queiroz (eds.) - 2008 - Berlin and New York: Springer.
    Edited in collaboration with FoLLI, the Association of Logic, Language and Information, this book constitutes the 4th volume of the FoLLI LNAI subline; containing the refereed proceedings of the 15th International Workshop on Logic, Language, Information and Computation, WoLLIC 2008, held in Edinburgh, UK, in July 2008. The 21 revised full papers presented together with the abstracts of 7 tutorials and invited lectures were carefully reviewed and selected from numerous submissions. The papers cover all pertinent subjects in computer science with (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On Implicational Intermediate Logics Axiomatizable by Formulas Minimal in Classical Logic: A Counter-Example to the Komori–Kashima Problem.Yoshiki Nakamura & Naosuke Matsuda - 2021 - Studia Logica 109 (6):1413-1422.
    The Komori–Kashima problem, that asks whether the implicational intermediate logics axiomatizable by formulas minimal in classical logic are only intuitionistic logic and classical logic, has stood for over a decade. In this paper, we give a counter-example to this problem. Additionally, we also give some open problems derived from this result.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • An ecumenical notion of entailment.Elaine Pimentel, Luiz Carlos Pereira & Valeria de Paiva - 2019 - Synthese 198 (S22):5391-5413.
    Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • On Dummett’s Pragmatist Justification Procedure.Hermógenes Oliveira - 2019 - Erkenntnis 86 (2):429-455.
    I show that propositional intuitionistic logic is complete with respect to an adaptation of Dummett’s pragmatist justification procedure. In particular, given a pragmatist justification of an argument, I show how to obtain a natural deduction derivation of the conclusion of the argument from, at most, the same assumptions.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Inference Rules and the Meaning of the Logical Constants.Hermógenes Oliveira - 2019 - Dissertation, Eberhard Karls Universität Tübingen
    The dissertation provides an analysis and elaboration of Michael Dummett's proof-theoretic notions of validity. Dummett's notions of validity are contrasted with standard proof-theoretic notions and formally evaluated with respect to their adequacy to propositional intuitionistic logic.
    Download  
     
    Export citation  
     
    Bookmark  
  • Analyticity, Balance and Non-admissibility of Cut in Stoic Logic.Susanne Bobzien & Roy Dyckhoff - 2018 - Studia Logica 107 (2):375-397.
    This paper shows that, for the Hertz–Gentzen Systems of 1933, extended by a classical rule T1 and using certain axioms, all derivations are analytic: every cut formula occurs as a subformula in the cut’s conclusion. Since the Stoic cut rules are instances of Gentzen’s Cut rule of 1933, from this we infer the decidability of the propositional logic of the Stoics. We infer the correctness for this logic of a “relevance criterion” and of two “balance criteria”, and hence that a (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Inconsistency-tolerant description logic. Part II: A tableau algorithm for CALC C.S. P. Odintsov & H. Wansing - 2008 - Journal of Applied Logic 6 (3):343-360.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
    Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Efficient exhaustive generation of functional programs using monte-carlo search with iterative deepening.Susumu Katayama - 2008 - In Tu-Bao Ho & Zhi-Hua Zhou (eds.), PRICAI 2008: Trends in Artificial Intelligence. Springer. pp. 199--210.
    Download  
     
    Export citation  
     
    Bookmark  
  • Constructing counter-models for modal logic K4 from refutation trees.Motohiko Mouri - 2002 - Bulletin of the Section of Logic 31 (2):81-90.
    Download  
     
    Export citation  
     
    Bookmark  
  • Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.
    Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Intuitionistic Socratic procedures.Tomasz F. Skura - 2005 - Journal of Applied Non-Classical Logics 15 (4):453-464.
    In the paper we study the method of Socratic proofs in the intuitionistic propositional logic as a reduction procedure. Our approach consists in constructing for a given sequent α a finite tree of sets of sequents by using invertible reduction rules of the kind: ? is valid if and only if ?1 is valid or... or ?n is valid. From such a tree either a Gentzen-style proof of α or an Aristotle-style refutation of α can also be extracted.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Decision methods for linearly ordered Heyting algebras.Sara Negri & Roy Dyckhoff - 2006 - Archive for Mathematical Logic 45 (4):411-422.
    The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Interpolation in non-classical logics.Giovanna D’Agostino - 2008 - Synthese 164 (3):421 - 435.
    We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
    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.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Uniform interpolation and the existence of sequent calculi.Rosalie Iemhoff - 2019 - Annals of Pure and Applied Logic 170 (11):102711.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
    An embedding of the implicational propositional intuitionistic logic into the nonmodal fragment of intuitionistic linear logic is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • On different intuitionistic calculi and embeddings from int to S.Uwe Egly - 2001 - Studia Logica 69 (2):249-277.
    In this paper, we compare several cut-free sequent systems for propositional intuitionistic logic Intwith respect to polynomial simulations. Such calculi can be divided into two classes, namely single-succedent calculi (like Gentzen's LJ) and multi-succedent calculi. We show that the latter allow for more compact proofs than the former. Moreover, for some classes of formulae, the same is true if proofs in single-succedent calculi are directed acyclic graphs (dags) instead of trees. Additionally, we investigate the effect of weakening rules on the (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2009 - Journal of Applied Non-Classical Logics 19 (2):149-166.
    Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Lyndon’s interpolation property for the logic of strict implication.Narbe Aboolian & Majid Alizadeh - 2022 - Logic Journal of the IGPL 30 (1):34-70.
    The main result proves Lyndon’s and Craig’s interpolation properties for the logic of strict implication ${\textsf{F}}$, with a purely syntactical method. A cut-free G3-style sequent calculus $ {\textsf{GF}} $ and its single-succedent variant $ \textsf{GF}_{\textsf{s}} $ are introduced. $ {\textsf{GF}} $ can be extended to a G3-variant of the sequent calculus GBPC3 for Visser’s basic logic. Also a simple syntactic proof of known embedding result of $ {\textsf{F}} $ into $ {\textsf{K}} $ is provided. An extension of $ {\textsf{F}} $, (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • An intuitionistic formula hierarchy based on high‐school identities.Taus Brock-Nannestad & Danko Ilik - 2019 - Mathematical Logic Quarterly 65 (1):57-79.
    We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e., sequent) isomorphisms corresponding to the high‐school identities, we show that one can obtain a more compact variant of a proof system, consisting of non‐invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalization procedure. Moreover, for (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation