Goal-Directed Calculi for Godel-Dummett Logics

摘要

In this work we present goal-directed calculi for the Godel-Dummett logic LC and its finite-valued counterparts, LC_n (n ≥ 2). We introduce a terminating hypersequent calculus for the implicational fragment of LC with local rules and a single identity axiom. We also give a labelled goal-directed calculus with invertible rules and show that it is co-NP. Finally we derive labelled goal-directed calculi for LC_n.