Description

• Title:
  Tautology Elimination, Cut Elimination, and S5
• Creator:
  Indrzejczak, Andrzej
• Description:
  Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As an illustration we present a cut-free sequent calculus for S5 based on tableau system of Fitting and prove admissibility of tautology elimination rule for it.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Date:
  2017.04.05
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 26 No. 4 (2017): December; 461-471;
  Logic and Logical Philosophy; Tom 26 Nr 4 (2017): December; 461-471;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/LLP.2017.005/11711
• Subject:
  sequent calculus;
  tautology elimination;
  cut elimination;
  modal logic S5
• Identifier: https://apcz.umk.pl/LLP/article/view/LLP.2017.005
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text