Agent Based Realtime Pedagogy For Proof Construction
Selmer Bringsjord, Paul Bello · 2020
There is a disturbing paradox at the heart of contemporary American education: As this education turns more and more "electronic," we are moving away from the one kind of learning that we know to be most effective, namely, one-on-one instruction.As the need for good teachers at the university level continues to grow, we see this paradox intensifying.And we see the problem manifesting itself in a particularly nasty way in curricula that predominantly focus on cultivating abstract reasoning ability in future scientists and engineers.The data tells us that as educators, we are not producing students able to successfully employ context-independent reasoning in technical domains.This is true despite the fact that there has been great progress made in developing educational technologies and aides for teaching formal, context -independent deductive reasoning; we refer here to an abundance of proof-construction environments.The fact is, teaching students to be good abstract reasoners requires the professor to have a one-on-one relationship with each student, with a keen eye on how each searches for a solution.The perfect automated logic instructor should be adaptable, and fully available to each student, at every time and every place.This is obviously not possible with human instruction, but our preliminary work suggests that our vision is capable of being realized in the digital domain: We are developing a suite of intelligent agents that bring the cutting edge in AI-based tutoring to the state-of-the-art in proof construction courseware.In addition, with agent-driven tutoring systems as a foundation, we aim to extend our agents so that they can be of assistance to logicians, mathematicians, and computer scientists in their research and development.Unfortunately, proof-construction environments in the educational realm, while presenting lucid proofs to the student, are based on weak theorem provers -provers that lack the sheer muscle to be of use to a professional scientist or engineer.We remedy the situation by using "industrial grade" theorem provers as the testbed for the development of our artificial assistants.