Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Refine search results

Results found: 1

first rewind previous Page / 1 next fast forward last

Search results

Search:
in the keywords:  modal logic S5
help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
1
Content available remote

Tautology Elimination, Cut Elimination, and S5

100%
EN
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.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.