A Decidable Temporal Relevant Logic for Time-Dependent Relevant Human Reasoning

摘要

In this paper, a Gentzen-type sequent calculus STRW is introduced for a new temporal relevant logic TRW which is obtained from the positive contraction-less relevant logic by adding some temporal operators. The cut-elimination and completeness theorems for STRW are proved. STRW is shown to be decidable and to have relevance principle.