18 found
Order:
  1.  15
    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 (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  2.  58
    Substructural Fuzzy Logics.George Metcalfe & Franco Montagna - 2007 - Journal of Symbolic Logic 72 (3):834 - 864.
    Substructural fuzzy logics are substructural logics that are complete with respect to algebras whose lattice reduct is the real unit interval [0.1]. In this paper, we introduce Uninorm logic UL as Multiplicative additive intuitionistic linear logic MAILL extended with the prelinearity axiom ((A → B) ∧ t) ∨ ((B → A) ∧ t). Axiomatic extensions of UL include known fuzzy logics such as Monoidal t-norm logic MTL and Gödel logic G, and new weakening-free logics. Algebraic semantics for these logics are (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   19 citations  
  3.  14
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  4.  38
    Structural Completeness in Fuzzy Logics.Petr Cintula & George Metcalfe - 2009 - Notre Dame Journal of Formal Logic 50 (2):153-182.
    Structural completeness properties are investigated for a range of popular t-norm based fuzzy logics—including Łukasiewicz Logic, Gödel Logic, Product Logic, and Hájek's Basic Logic—and their fragments. General methods are defined and used to establish these properties or exhibit their failure, solving a number of open problems.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  5.  52
    Craig Interpolation for Semilinear Substructural Logics.Enrico Marchioni & George Metcalfe - 2012 - Mathematical Logic Quarterly 58 (6):468-481.
    The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R-mingle with unit” logic that have the Craig interpolation property. This latter characterization is obtained using a model-theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  51
    Analytic Calculi for Product Logics.George Metcalfe, Nicola Olivetti & Dov Gabbay - 2004 - Archive for Mathematical Logic 43 (7):859-889.
    Product logic Π is an important t-norm based fuzzy logic with conjunction interpreted as multiplication on the real unit interval [0,1], while Cancellative hoop logic CHL is a related logic with connectives interpreted as for Π but on the real unit interval with 0 removed (0,1]. Here we present several analytic proof systems for Π and CHL, including hypersequent calculi, co-NP labelled calculi and sequent calculi.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  7.  72
    Fuzzy Logics Based on [0,1)-Continuous Uninorms.Dov Gabbay & George Metcalfe - 2007 - Archive for Mathematical Logic 46 (5-6):425-449.
    Axiomatizations are presented for fuzzy logics characterized by uninorms continuous on the half-open real unit interval [0,1), generalizing the continuous t-norm based approach of Hájek. Basic uninorm logic BUL is defined and completeness is established with respect to algebras with lattice reduct [0,1] whose monoid operations are uninorms continuous on [0,1). Several extensions of BUL are also introduced. In particular, Cross ratio logic CRL, is shown to be complete with respect to one special uninorm. A Gentzen-style hypersequent calculus is provided (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  8.  38
    Giles’s Game and the Proof Theory of Łukasiewicz Logic.Christian G. Fermüller & George Metcalfe - 2009 - Studia Logica 92 (1):27 - 61.
    In the 1970s, Robin Giles introduced a game combining Lorenzen-style dialogue rules with a simple scheme for betting on the truth of atomic statements, and showed that the existence of winning strategies for the game corresponds to the validity of formulas in Łukasiewicz logic. In this paper, it is shown that ‘disjunctive strategies’ for Giles’s game, combining ordinary strategies for all instances of the game played on the same formula, may be interpreted as derivations in a corresponding proof system. In (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  7
    Giles’s Game and the Proof Theory of Łukasiewicz Logic.Christian G. Fermüller & George Metcalfe - 2009 - Studia Logica 92 (1):27-61.
    In the 1970s, Robin Giles introduced a game combining Lorenzen-style dialogue rules with a simple scheme for betting on the truth of atomic statements, and showed that the existence of winning strategies for the game corresponds to the validity of formulas in Łukasiewicz logic. In this paper, it is shown that ' disjunctive strategies' for Giles's game, combining ordinary strategies for all instances of the game played on the same formula, may be interpreted as derivations in a corresponding proof system. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  10.  5
    Uniform Interpolation and Coherence.Tomasz Kowalski & George Metcalfe - 2019 - Annals of Pure and Applied Logic 170 (7):825-841.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11.  23
    A Sequent Calculus for Constructive Logic with Strong Negation as a Substructural Logic.George Metcalfe - 2009 - Bulletin of the Section of Logic 38 (1/2):1-7.
  12.  52
    Normal Forms for Fuzzy Logics: A Proof-Theoretic Approach. [REVIEW]Petr Cintula & George Metcalfe - 2007 - Archive for Mathematical Logic 46 (5-6):347-363.
    A method is described for obtaining conjunctive normal forms for logics using Gentzen-style rules possessing a special kind of strong invertibility. This method is then applied to a number of prominent fuzzy logics using hypersequent rules adapted from calculi defined in the literature. In particular, a normal form with simple McNaughton functions as literals is generated for łukasiewicz logic, and normal forms with simple implicational formulas as literals are obtained for Gödel logic, Product logic, and Cancellative hoop logic.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  13.  9
    Expressivity in Chain-Based Modal Logics.Michel Marti & George Metcalfe - 2018 - Archive for Mathematical Logic 57 (3-4):361-380.
    We investigate the expressivity of many-valued modal logics based on an algebraic structure with a complete linearly ordered lattice reduct. Necessary and sufficient algebraic conditions for admitting a suitable Hennessy–Milner property are established for classes of image-finite and modally saturated models. Full characterizations are obtained for many-valued modal logics based on complete BL-chains that are finite or have the real unit interval [0, 1] as a lattice reduct, including Łukasiewicz, Gödel, and product modal logics.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  14.  7
    Uniform Interpolation and Compact Congruences.Samuel J. van Gool, George Metcalfe & Constantine Tsinakis - 2017 - Annals of Pure and Applied Logic 168 (10):1927-1948.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15.  14
    Unifiability and Admissibility in Finite Algebras.George Metcalfe & Christoph Röthlisberger - 2012 - In S. Barry Cooper (ed.), How the World Computes. pp. 485--495.
    Direct download  
     
    Export citation  
     
    Bookmark  
  16.  9
    Łukasiewicz Logic: From Proof Systems To Logic Programming.George Metcalfe, Nicola Olivetti & Dov Gabbay - 2005 - Logic Journal of the IGPL 13 (5):561-585.
    We present logic programming style “goal-directed” proof methods for Łukasiewicz logic Ł that both have a logical interpretation, and provide a suitable basis for implementation. We introduce a basic version, similar to goal-directed calculi for other logics, and make refinements to improve efficiency and obtain termination. We then provide an algorithm for fuzzy logic programming in Rational Pavelka logic RPL, an extension of Ł with rational constants.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  17.  5
    Special Issue on Admissible Rules and Unification.Rosalie Iemhoff & George Metcalfe - 2016 - Notre Dame Journal of Formal Logic 57 (4):441-442.
  18.  4
    Proof Theory for Lattice-Ordered Groups.Nikolaos Galatos & George Metcalfe - 2016 - Annals of Pure and Applied Logic 167 (8):707-724.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark