---
title: "Automatically Generating Problems and Solutions for Natural Deduction"
authors:
  - "Umair Z. Ahmed"
  - "Sumit Gulwani"
  - "Amey Karkare"
doi: ""
url: "https://ijcai.org/proceedings/2013/291"
pdf: "https://ijcai.org/proceedings/2013/0291.pdf"
venue: "Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence"
year: 2013
pages: "1968-1974"
track: ""
keywords:
---

# Automatically Generating Problems and Solutions for Natural Deduction

Umair Z. Ahmed, Sumit Gulwani, Amey Karkare

*Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence*, pages 1968-1974.

## 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.