Using Automated Theorem Provers to Teach Knowledge Representation in First-Order Logic

TL;DR

This paper presents an automated grading system using a theorem prover to help undergraduate AI students learn first-order logic knowledge representation more effectively, with significant improvements in exam performance.

Contribution

It introduces a novel automated assessment system employing a resolution theorem prover for first-order logic exercises in AI education, enhancing student learning outcomes.

Findings

Significant improvement in student exam scores.

Effective automated feedback for logic exercises.

Potential for richer formative feedback methods.

Abstract

Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the assignment of numerous exercises involving the formulation of some bit of knowledge, communicated using a natural language such as English, as a sentence in some logic. The number of such exercises needed to master this skill is far too large to allow typical artificial intelligence course teaching teams to provide prompt feedback on student efforts. Thus, an automated assessment system for such exercises is needed to ensure that students receive an adequate amount of practice, with the rapid delivery of feedback allowing students to identify errors in their understanding and correct them. This paper describes an automated grading system for knowledge representation exercises using first-order logic. A resolution theorem prover, \textit{Prover9}, is used to check if a student-submitted formula is logically equivalent to a solution provided by the instructor. This system has been used by students enrolled in undergraduate artificial intelligence classes for several years. Use of this teaching tool resulted in a statistically significant improvement on first-order logic knowledge representation questions appearing on the course final examination. This article explains how this system works, provides an analysis of changes in student learning outcomes, and explores potential enhancements of this system, including the possibility of providing rich formative feedback by replacing the resolution theorem prover with a tableaux-based method.