A Gentzen-style extension of natural deduction -- adjusted for undergraduate informatics studies

Abstract

We consider logical proof description formalisms presented to undergraduate informatics students studying AI. We argue that pure natural deduction framework is short in well-known logical consequences which can be used in appropriate proof searching exercises for informatics students. Therefore, we propose to borrow some new deduction rules of Gentzen calculus adjusted to the formal requirements of natural deduction. In this way we mix the advantages of both natural deduction and Gentzen calculus. Namely, we keep that we have one goal in every state of the proof (like in natural deduction and in our intuitive thinking) but the proof of the propositional logical laws can be produced semi-automatically and the student can solve serious deduction tasks occuring in practical applications of AI (like with Gentzen calculus).