21 found
Order:
  1.  31
    Valentini's Cut-Elimination for Provability Logic Resolved.Rajeev Gore & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
    In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There is (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  2. 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 ϕ. Moreover, (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  3. Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-Free Deep Inference Calculi for S.Rajeev Gore - manuscript
  4. 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.
    Direct download  
     
    Export citation  
     
    My bibliography  
  5.  46
    Free-Variable Tableaux for Propositional Modal Logics.Bernhard Beckert & Rajeev GorÉ - 2001 - Studia Logica 69 (1):59-96.
    Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  6.  16
    A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics.Rajeev Gore - unknown
    We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma for regular grammar (...)
    Direct download  
    Translate
     
     
    Export citation  
     
    My bibliography   1 citation  
  7.  19
    Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs.Rajeev Gore - manuscript
  8.  33
    System Description: The Tableaux Work Bench.Rajeev Gore - manuscript
    The Tableaux Work Bench (TWB) is a meta tableau system designed for logicians with limited programming or automatic reasoning knowledge to experiment with new tableau calculi and new decision procedures. It has a simple interface, a history mechanism for controlling loops or pruning the search space, and modal simplification.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  9.  37
    Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics.Rajeev Goré - 1994 - Studia Logica 53 (3):433 - 457.
    We present sound, (weakly) complete and cut-free tableau systems for the propositional normal modal logicsS4.3, S4.3.1 andS4.14. When the modality is given a temporal interpretation, these logics respectively model time as a linear dense sequence of points; as a linear discrete sequence of points; and as a branching tree where each branch is a linear discrete sequence of points.Although cut-free, the last two systems do not possess the subformula property. But for any given finite set of formulaeX the superformulae involved (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  10.  32
    Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Gore, Linda Postniece & Alwen Tiu - unknown
    We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  11.  29
    A Cut-Free Sequent Calculus for Bi-Intuitionistic Logic.Rajeev Gore - manuscript
  12.  19
    Advances in Modal Logic, Volume.Rajeev Gore - unknown
    We study a propositional bimodal logic consisting of two S4 modalities and [a], together with the interaction axiom scheme a ϕ → a ϕ. In the intended semantics, the plain..
    Direct download  
     
    Export citation  
     
    My bibliography  
  13.  8
    Errata to Cambridge Computer Laboratory Technical Report Number 257: Cut-Free Sequent and Tableau Systems for Propositional Normal Modal Logics By.Rajeev Gore - unknown
    The main technical errors are in the literature survey. On pages 44, 93-94, 131 and 133 I claim that Fitting's and/or Rautenberg's systems are incomplete because they omit contraction. The claim is wrong because contraction is implicit in their set notation. Their systems are complete because they allow contraction on any formula whereas the systems in this technical report explicitly build contraction into certain rules, allowing contraction only on certain types of formulae. Please accept my apologies for any confusion this (...)
    Direct download  
    Translate
     
     
    Export citation  
     
    My bibliography  
  14.  11
    Displaying Modal Logic, Heinrich Wansing.Rajeev Goré - 2000 - Journal of Logic, Language and Information 9 (2):269-272.
  15.  8
    Display Calculi for Logics with Relative Accessibility Relations.Stéphane Demri & Rajeev Goré - 2000 - Journal of Logic, Language and Information 9 (2):213-236.
    We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  16.  4
    Cut-Elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
    We present a syntactic proof of cut-elimination for weak Grzegorczyk logic Go. The logic has a syntactically similar axiomatisation to Gödel–Löb logic GL (provability logic) and Grzegorczyk’s logic Grz. Semantically, GL can be viewed as the irreflexive counterpart of Go, and Grz can be viewed as the reflexive counterpart of Go. Although proofs of syntactic cut-elimination for GL and Grz have appeared in the literature, this is the first proof of syntactic cut-elimination for Go. The proof is technically interesting, requiring (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  17.  2
    Review: Sally Popkorn, First Steps in Modal Logic. [REVIEW]Rajeev Gore - 1996 - Journal of Symbolic Logic 61 (3):1055-1056.
  18.  1
    Editorial.Krysia Broda, Marcello D'agostino, Rajeev Gore, Rob Johnson & Steve Reeves - 1995 - Logic Journal of the IGPL 3 (6):826-826.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  19.  3
    One-Pass Tableaux for Computation Tree Logic.Rajeev Gore - manuscript
  20. On the Completeness of Classical Modal Display Logic.Rajeev Goré - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 2--137.
     
    Export citation  
     
    My bibliography  
  21. Sally Popkorn . First Steps in Modal Logic. Cambridge University Press, Cambridge 1994, and New York and Oakleigh, Victoria, 1995, Xiii + 314 Pp. [REVIEW]Rajeev Goré - 1996 - Journal of Symbolic Logic 61 (3):1055-1056.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography