@techreport{R20,
  key    =       {R20},
  author =	 {Quoc Bao Vo and Christoph Benzm{\"u}ller and Serge Autexier},
  title =	 {An Approach to Assertion Application via Generalized Resolution},
  institution =	 {Fachrichtung Informatik, Universit{\"a}t des Saarlandes,
                  Saarbr{\"u}cken, Germany},
  year =	 2003,
  type =	 {SEKI Report (ISSN 1437-4447)},
  number =	 {SR-03-01},
  abstract =	 {In this paper we address assertion retrieval and application in theorem
                  proving systems or proof planning systems for classical first-order
                  logic. Due to Huang the notion of assertion comprises mathematical
                  knowledge from a mathematical knowledge base KB such as definitions,
                  theorems, and axioms. %, as well as assumptions generated within the
                  prover during proof construction. We propose a distributed mediator
                  module between KB and a theorem proving system S which is independent of
                  the particular proof representation format of S and which applies
                  generalized resolution in order to analyze the logical consequences of
                  arbitrary assertions for a proof context at hand. Our approach is
                  applicable without any extension also to the assumptions that are
                  dynamically created during a proof search process. It therefore realizes
                  a crucial first step towards full automation of assertion level
                  reasoning. We discuss the benefits and connection of our approach to
                  proof planning and motivate an application in a project aiming at a
                  tutorial dialogue system for mathematics.},
}