Switch to: References

Add citations

You must login to add citations.
  1. Admissible Bases Via Stable Canonical Rules.Nick Bezhanishvili, David Gabelaia, Silvio Ghilardi & Mamuka Jibladze - 2016 - Studia Logica 104 (2):317-341.
    We establish the dichotomy property for stable canonical multi-conclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Filtering unification and most general unifiers in modal logic.Silvio Ghilardi & Lorenzo Sacchetti - 2004 - Journal of Symbolic Logic 69 (3):879-906.
    We characterize (both from a syntactic and an algebraic point of view) the normal K4-logics for which unification is filtering. We also give a sufficient semantic criterion for existence of most general unifiers, covering natural extensions of K4.2⁺ (i.e., of the modal system obtained from K4 by adding to it, as a further axiom schemata, the modal translation of the weak excluded middle principle).
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Remarks about the unification type of several non-symmetric non-transitive modal logics.Philippe Balbiani - 2019 - Logic Journal of the IGPL 27 (5):639-658.
    The problem of unification in a normal modal logic $L$ can be defined as follows: given a formula $\varphi$, determine whether there exists a substitution $\sigma$ such that $\sigma $ is in $L$. In this paper, we prove that for several non-symmetric non-transitive modal logics, there exists unifiable formulas that possess no minimal complete set of unifiers.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Proof theory for admissible rules.Rosalie Iemhoff & George Metcalfe - 2009 - Annals of Pure and Applied Logic 159 (1-2):171-186.
    Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor (...)
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • The Basic Intuitionistic Logic of Proofs.Sergei Artemov & Rosalie Iemhoff - 2007 - Journal of Symbolic Logic 72 (2):439 - 451.
    The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Proving Cleanthes wrong.Laureano Luna - 2021 - Journal of Applied Logic 8 (3):707-736.
    Hume’s famous character Cleanthes claims that there is no difficulty in explaining the existence of causal chains with no first cause since in them each item is causally explained by its predecessor. Relying on logico-mathematical resources, we argue for two theses: (1) if the existence of Cleanthes’ chain can be explained at all, it must be explained by the fact that the causal law ruling it is in force, and (2) the fact that such a causal law is in force (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • KD is nullary.Philippe Balbiani & Çiğdem Gencer - 2017 - Journal of Applied Non-Classical Logics 27 (3-4):196-205.
    In the ordinary modal language, KD is the modal logic determined by the class of all serial frames. In this paper, we demonstrate that KD is nullary.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Unification in modal logic Alt1.Philippe Balbiani & Tinko Tinchev - 2016 - In Lev Beklemishev, Stéphane Demri & András Máté (eds.), Advances in Modal Logic, Volume 11. CSLI Publications. pp. 117-134.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Unification in epistemic logics.Philippe Balbiani & Çiğdem Gencer - 2017 - Journal of Applied Non-Classical Logics 27 (1-2):91-105.
    Epistemic logics are essential to the design of logical systems that capture elements of reasoning about knowledge. In this paper, we study the computability of unifiability and the unification types in several epistemic logics.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Almost structural completeness; an algebraic approach.Wojciech Dzik & Michał M. Stronkowski - 2016 - Annals of Pure and Applied Logic 167 (7):525-556.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • A Syntactic Approach to Unification in Transitive Reflexive Modal Logics.Rosalie Iemhoff - 2016 - Notre Dame Journal of Formal Logic 57 (2):233-247.
    This paper contains a proof-theoretic account of unification in transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are presented and these results are extended to negationless fragments. In particular, a syntactic proof of Ghilardi’s result that $\mathsf {S4}$ has finitary unification is provided. In this approach the relation between classical valuations, projective unifiers, and admissible rules is clarified.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Unification, finite duality and projectivity in varieties of Heyting algebras.Silvio Ghilardi - 2004 - Annals of Pure and Applied Logic 127 (1-3):99-115.
    We investigate finitarity of unification types in locally finite varieties of Heyting algebras, giving both positive and negative results. We make essential use of finite dualities within a conceptualization for E-unification theory 733–752) relying on the algebraic notion of a projective object.
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  • Unifiability and Structural Completeness in Relation Algebras and in Products of Modal Logic S5.Wojciech Dzik & Beniamin Wróbel - 2015 - Bulletin of the Section of Logic 44 (1/2):1-14.
    Unifiability of terms (and formulas) and structural completeness in the variety of relation algebras RA and in the products of modal logic S5 is investigated. Nonunifiable terms (formulas) which are satisfiable in varieties (in logics) are exhibited. Consequently, RA and products of S5 as well as representable diagonal-free n-dimensional cylindric algebras, RDfn, are almost structurally complete but not structurally complete. In case of S5n a basis for admissible rules and the form of all passive rules are provided.
    Download  
     
    Export citation  
     
    Bookmark  
  • Admissible rules for six intuitionistic modal logics.Iris van der Giessen - 2023 - Annals of Pure and Applied Logic 174 (4):103233.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Remarks about the unification types of some locally tabular normal modal logics.Philippe Balbiani, ÇiĞdem Gencer, Maryam Rostamigiv & Tinko Tinchev - 2023 - Logic Journal of the IGPL 31 (1):115-139.
    It is already known that unifiable formulas in normal modal logic |$\textbf {K}+\square ^{2}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{2}\bot $| are unitary. In this paper, we prove that for all |$d{\geq }3$|⁠, unifiable formulas in normal modal logic |$\textbf {K}+\square ^{d}\bot $| are either finitary or unitary and unifiable formulas in normal modal logic |$\textbf {Alt}_{1}+\square ^{d}\bot $| are unitary.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Almost structurally complete infinitary consequence operations extending S4.3.Wojciech Dzik & Piotr Wojtylak - 2015 - Logic Journal of the IGPL 23 (4):640-661.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Rules with parameters in modal logic I.Emil Jeřábek - 2015 - Annals of Pure and Applied Logic 166 (9):881-933.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • On unification and admissible rules in Gabbay–de Jongh logics.Jeroen P. Goudsmit & Rosalie Iemhoff - 2014 - Annals of Pure and Applied Logic 165 (2):652-672.
    In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Frege systems for extensible modal logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.
    By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 36–50; R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 129–146] have recently shown p-equivalence of (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Hereditarily Structurally Complete Intermediate Logics: Citkin’s Theorem Via Duality.Nick Bezhanishvili & Tommaso Moraschini - 2023 - Studia Logica 111 (2):147-186.
    A deductive system is said to be structurally complete if its admissible rules are derivable. In addition, it is called hereditarily structurally complete if all its extensions are structurally complete. Citkin (1978) proved that an intermediate logic is hereditarily structurally complete if and only if the variety of Heyting algebras associated with it omits five finite algebras. Despite its importance in the theory of admissible rules, a direct proof of Citkin’s theorem is not widely accessible. In this paper we offer (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • About the Unification Type of Modal Logics Between.Philippe Balbiani & Çiğdem Gencer - 2020 - Studia Logica 108 (5):941-966.
    The unification problem in a normal modal logic is to determine, given a formula.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Unification and admissible rules for paraconsistent minimal Johanssonsʼ logic J and positive intuitionistic logic IPC.Sergei Odintsov & Vladimir Rybakov - 2013 - Annals of Pure and Applied Logic 164 (7-8):771-784.
    We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic IPC+. This paper proves that the problem of admissibility for inference rules with coefficients is decidable for the paraconsistent minimal Johanssonsʼ logic J and the positive intuitionistic logic IPC+. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. Checking just unifiability (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Projective unification in transitive modal logics.Sławomir Kost - 2018 - Logic Journal of the IGPL 26 (5):548-566.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Structural Completeness in Substructural Logics.J. S. Olson, J. G. Raftery & C. J. Van Alten - 2008 - Logic Journal of the IGPL 16 (5):453-495.
    Hereditary structural completeness is established for a range of substructural logics, mainly without the weakening rule, including fragments of various relevant or many-valued logics. Also, structural completeness is disproved for a range of systems, settling some previously open questions.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Best Unifiers in Transitive Modal Logics.Vladimir V. Rybakov - 2011 - Studia Logica 99 (1-3):321-336.
    This paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4 : S4 itself, K4, Grz and Gödel-Löb provability logic GL . As a result, new, but not the first, algorithms for the construction of ‘best’ unifiers in these logics are being proposed. The proposed algorithms are based on our earlier approach to solve in an algorithmic way the admissibility problem of inference rules for S4 and Grz . The first algorithms for (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Two decision problems in Contact Logics.Philippe Balbiani, Çiğdem Gencer & Zafer Özdemir - 2019 - Logic Journal of the IGPL 27 (1):8-32.
    Contact Logics provide a natural framework for representing and reasoning about regions in several areas of computer science. In this paper, we focus our attention on reasoning methods for Contact Logics and address the satisfiability problem and the unifiability problem. Firstly, we give sound and complete tableaux-based decision procedures in Contact Logics and we obtain new results about the decidability/complexity of the satisfiability problem in these logics. Secondly, we address the computability of the unifiability problem in Contact Logics and we (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Modal Consequence Relations Extending $mathbf{S4.3}$: An Application of Projective Unification.Wojciech Dzik & Piotr Wojtylak - 2016 - Notre Dame Journal of Formal Logic 57 (4):523-549.
    We characterize all finitary consequence relations over S4.3, both syntactically, by exhibiting so-called passive rules that extend the given logic, and semantically, by providing suitable strongly adequate classes of algebras. This is achieved by applying an earlier result stating that a modal logic L extending S4 has projective unification if and only if L contains S4.3. In particular, we show that these consequence relations enjoy the strong finite model property, and are finitely based. In this way, we extend the known (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Admissible rules in the implication–negation fragment of intuitionistic logic.Petr Cintula & George Metcalfe - 2010 - Annals of Pure and Applied Logic 162 (2):162-171.
    Uniform infinite bases are defined for the single-conclusion and multiple-conclusion admissible rules of the implication–negation fragments of intuitionistic logic and its consistent axiomatic extensions . A Kripke semantics characterization is given for the structurally complete implication–negation fragments of intermediate logics, and it is shown that the admissible rules of this fragment of form a PSPACE-complete set and have no finite basis.
    Download  
     
    Export citation  
     
    Bookmark   24 citations  
  • Complexity of admissible rules.Emil Jeřábek - 2007 - Archive for Mathematical Logic 46 (2):73-92.
    We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • Canonical Rules.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (4):1171 - 1205.
    We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  • Unifiers in transitive modal logics for formulas with coefficients.V. Rybakov - 2013 - Logic Journal of the IGPL 21 (2):205-215.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Unification in linear temporal logic LTL.Sergey Babenyshev & Vladimir Rybakov - 2011 - Annals of Pure and Applied Logic 162 (12):991-1000.
    We prove that a propositional Linear Temporal Logic with Until and Next has unitary unification. Moreover, for every unifiable in LTL formula A there is a most general projective unifier, corresponding to some projective formula B, such that A is derivable from B in LTL. On the other hand, it can be shown that not every open and unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier.
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • Unification in first-order transitive modal logic.Wojciech Dzik & Piotr Wojtylak - forthcoming - Logic Journal of the IGPL.
    Download  
     
    Export citation  
     
    Bookmark  
  • Preservation of admissible rules when combining logics.João Rasga, Cristina Sernadas & Amílcar Sernadas - 2016 - Review of Symbolic Logic 9 (4):641-663.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • On Rules.Rosalie Iemhoff - 2015 - Journal of Philosophical Logic 44 (6):697-711.
    This paper contains a brief overview of the area of admissible rules with an emphasis on results about intermediate and modal propositional logics. No proofs are given but many references to the literature are provided.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Discrete linear temporal logic with current time point clusters, deciding algorithms.V. Rybakov - 2008 - Logic and Logical Philosophy 17 (1-2):143-161.
    The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Undecidability of admissibility in the product of two Alt logics.Philippe Balbiani & Çiğdem Gencer - forthcoming - Logic Journal of the IGPL.
    The product of two $\textbf {Alt}$ logics possesses the polynomial product finite model property and its membership problem is $\textbf {coNP}$-complete. Using a reduction from an undecidable domino-tiling problem, we prove that its admissibility problem is undecidable.
    Download  
     
    Export citation  
     
    Bookmark  
  • Universal proof theory: Feasible admissibility in intuitionistic modal logics.Amirhossein Akbar Tabatabai & Raheleh Jalali - 2025 - Annals of Pure and Applied Logic 176 (2):103526.
    Download  
     
    Export citation  
     
    Bookmark  
  • Unification in Pretabular Extensions of S4.Stepan I. Bashmakov - 2021 - Logica Universalis 15 (3):381-397.
    L.L. Maksimova and L. Esakia, V. Meskhi showed that the modal logic \ has exactly 5 pretabular extensions PM1–PM5. In this paper, we study the problem of unification for all given logics. We showed that PM2 and PM3 have finitary, and PM1, PM4, PM5 have unitary types of unification. Complete sets of unifiers in logics are described.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (15 other versions)2010 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '10.Uri Abraham & Ted Slaman - 2011 - Bulletin of Symbolic Logic 17 (2):272-329.
    Download  
     
    Export citation  
     
    Bookmark  
  • Unification types in Euclidean modal logics.Majid Alizadeh, Mohammad Ardeshir, Philippe Balbiani & Mojtaba Mojtahedi - 2023 - Logic Journal of the IGPL 31 (3):422-440.
    We prove that $\textbf {K}5$ and some of its extensions that do not contain $\textbf {K}4$ are of unification type $1$.
    Download  
     
    Export citation  
     
    Bookmark  
  • Projective formulas and unification in linear temporal logic LTLU.V. Rybakov - 2014 - Logic Journal of the IGPL 22 (4):665-672.
    Download  
     
    Export citation  
     
    Bookmark  
  • Unification in superintuitionistic predicate logics and its applications.Wojciech Dzik & Piotr Wojtylak - 2019 - Review of Symbolic Logic 12 (1):37-61.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Unification in intermediate logics.Rosalie Iemhoff & Paul Rozière - 2015 - Journal of Symbolic Logic 80 (3):713-729.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Finitary unification in locally tabular modal logics characterized.Wojciech Dzik, Sławomir Kost & Piotr Wojtylak - 2022 - Annals of Pure and Applied Logic 173 (4):103072.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Unification with parameters in the implication fragment of classical propositional logic.Philippe Balbiani & Mojtaba Mojtahedi - 2022 - Logic Journal of the IGPL 30 (3):454-464.
    In this paper, we show that the implication fragment of classical propositional logic is finitary for unification with parameters.
    Download  
     
    Export citation  
     
    Bookmark  
  • Independent bases of admissible rules.Emil Jerábek - 2008 - Logic Journal of the IGPL 16 (3):249-267.
    We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  • Unifiability in extensions of K4.Çiğdem Gencer & Dick de Jongh - 2009 - Logic Journal of the IGPL 17 (2):159-172.
    We extend and generalize the work on unifiability of [8]. We give a semantic characterization for unifiability and non-unifiability in the extensions of K4. We apply this in particular to extensions of KD4, GL and K4.3 to obtain a syntactic characterization and give a concrete decision procedure for unifiability for those logics. For that purpose we use universal models.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Unification types and union splittings in intermediate logics.Wojciech Dzik, Sławomir Kost & Piotr Wojtylak - 2025 - Annals of Pure and Applied Logic 176 (1):103508.
    Download  
     
    Export citation  
     
    Bookmark