User System Interaction Within Theorema Extended Abstract
Koji Nakagawa, Felix Kossak · Electronic Notes in Theoretical Computer Science · 1999
The purpose of Theorema is to provide various ranges of users, from students to experts of mathematics, with an integrated environment for computing, solving, and proving. To make the system convenient, it is necessary to have sophisticated user system interaction. In this paper we discuss the user system interaction of Theorema from two aspects, namely remote interaction with Theorema over the internet and user — prover interaction within Theorema. The remote interaction increases the possibilities of using the system in various situations and of collaborative work. The user — prover interaction allows us to combine the proving power of fully automated provers and human creativity as well as to train students.