A task-oriented agent-based mechanism for theorem proving

We present an agent-based mechanism that acts as a mediator module between theorem proving systems and mathematical knowledge bases containing information that is necessary for the constructions of proofs. Unlike the more popular user-oriented mediators who work as information agents to provide the so-called value-added services to the collected data before presenting it to users or user applications, our (multi-)agents are more task-oriented. That is, our agents work in tandem with the user or user application on the tasks the user is trying to solve. This approach is particularly suitable to mathematical knowledge retrieval in theorem proving as (i) checking for applicable axioms/definitions/theorems from the knowledge base can be done independently from the proof search process concurrently carried out by the prover, and (ii) the prover and the mediator operate on two different search spaces and the search outcome brought about by the mediator can be of great benefit to the prover, e.g. to avoid the prover from exploring many unnecessary or irrelevant proof steps, to keep the prover´s search space more manageable and the constructed proof more comprehensible.