Automatically Generating Problems and Solutions for Natural Deduction
Natural deduction, which is a method for establishing validity of propositional type arguments, helps develop important reasoning skills and is thus a key ingredient in a course on introductory logic. We present two core components, namely solution generation and practice problem generation, for enabling computer-aided education for this important subject domain. The key enabling technology is use of an offline-computed data-structure called Universal Proof Graph (UPG) that encodes all possible applications of inference rules over all small propositions abstracted using their bitvector-based truth-table representation. This allows an efficient forward search for solution generation. More interestingly, this allows generating fresh practice problems
that have given solution characteristics by performing a backward search in UPG. We obtained
500+ natural deduction problems from various textbooks. Our solution generation procedure can solve many more problems than the traditional forward chaining based procedure, while our problem generation procedure can efficiently generate several variants with desired characteristics.