Understanding and extending an implemented reasoning system

Humans mentally model complex and highly structured environments and effortlessly draw immediate conclusions from what they know about these environments. In this project, we have implemented a "proof assistant" system capable of doing exactly these things, though not as well as humans. Researchers at both graduate and undergraduate levels are invited to learn about this implementation, experiment with it, and propose/implement extensions to the system.

Ideal candidates will be very strong in both mathematical aptitude and computer programming skills. Candidates will learn some of the LISP programming language as well as some formal mathematical logic. Ideal coursework background is ECE 368 (Datastructures and Algorithms) and ECE 369 (Discrete Mathematics), or the equivalent background from other departments or universities. Candidates lacking this background can be considered but will spend much more time coming up to speed.

I can offer 3 credit versions of this project to those interested in a single-semester investment, at either the graduate or undergraduate level. Larger and more ambitious variants are available for MS thesis projects. It may be possible to arrange either of these options at universities outside Purdue for strongly qualified and motivated candidates.