A natural deduction calculus for gödel-dummett logic internalizing proof-search control mechanisms?

We introduce a natural deduction calculus for the Gödel- Dummett Logic LC semantically characterized by linearly ordered Kripke models. Our calculus is inspired by an analogous calculus for Intuitionistic logic (IPL) internalizing mechanisms to reduce the proof-search space that has been used to define a goal-oriented proof-search procedure for IPL. In this paper we present the calculus for LC and we sketch its soundness and completeness.