@inproceedings{ahmed2013automatically,
author = {Ahmed, Umair Z. and Gulwani, Sumit and Karkare, Amey},
title = {Automatically Generating Problems and Solutions for Natural Deduction},
booktitle = {IJCAI '13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence},
year = {2013},
month = {August},
abstract = {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 around 300 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.},
url = {http://approjects.co.za/?big=en-us/research/publication/automatically-generating-problems-solutions-natural-deduction/},
pages = {1968-1975},
isbn = {978-1-57735-633-2},
edition = {IJCAI '13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence},
}