arnold beckmann's pages
Hyper Natural Deduction
Author: Arnold Beckmann and Norbert Preining
Title: Hyper Natural Deduction
Proceedings: Logic in Computer Science (LICS), 2015, 30th Annual ACM/IEEE Symposium on
Pages: 547 - 558
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.