Arnold Beckmann and Norbert Preining
Symposium on Logic in Computer Science (LICS), 2015, 30th Annual ACM/IEEE. Pages: 547 - 558
Publication year: 2015

We introduce a Hyper Natural Deduction system as an extension of Gentzen’s Natural Deduction system. A Hyper Natural Deduction consists of a finite set of derivations which may use, beside typical Natural Deduction rules, additional rules providing means for communication between derivations. We show that our Hyper Natural Deduction system is sound and complete for infinite-valued propositional Gòˆdel Logic, by giving translations to and from Avron’s Hyper sequent Calculus. We also provide conversions for normalisation and prove the existence of normal forms for our Hyper Natural Deduction system.