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.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Pawlak had proposed the notion of rough truth in 1987 [16]. The article takes a fresh look at this ``soft'' truth, and presents a formal system LR, that is shown to be sound and complete with respect to a semantics determined by this notion. LR is based on the modal logic S5. Notable is the rough consequence relation defining LR (a first version introduced in [9]), and rough consistency (also introduced in [9]), used to prove the completeness result. The former is defined in order to be able to derive roughly true propositions from roughly true premisses in an information system. The motivation for the latter stems from the observation that a proposition and its negation may well be roughly true together. A characterization of LR-consequence shows that the paraconsistent discussive logic J of Ja\'skowski is equivalent to LR. So, LR, developed from a totally independent angle, viz. that of rough set theory, gives an alternative formulation to this well-studied logic. It is further observed that pre-rough logic [3] and 3-valued ukasiewicz logic are embeddable into LR.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.