Assertion application in theorem proving and proof planning

Our work addresses assertion retrieval and application in theorem proving systems or proof planning systems for classical firstorder logic. We propose a distributed mediator M between a mathematical knowledge base KB and a theorem proving system TP which is independent of the particular proof and knowledge representation formats of TP and KB and which applies generalized resolution in order to analyze the logical consequences of arbitrary assertions for a proof context at hand. We discuss the connection to proof planning and motivate an application in a project aiming at a tutorial dialogue system for mathematics.