@techreport{R21,
  key    =       {R21},
  author =	 {Serge Autexier and Christoph Benzm{\"u}ller and Dieter Hutter},
  title =	 {Towards a Framework to Integrate Proof Search Paradigms},
  institution =	 {Fachrichtung Informatik, Universit{\"a}t des Saarlandes,
                  Saarbr{\"u}cken, Germany},
  year =	 2003,
  type =	 {SEKI Report (ISSN 1437-4447)},
  number =	 {SR-03-02},
  abstract =	 {Research on automated and interactive theorem proving aims at the
                  mechanization of logical reasoning. Aside from the development of logic
                  calculi it became rapidly apparent that the organization of proof search
                  on top of the calculi is an essential task in the design of powerful
                  theorem proving systems. Different paradigms of how to organize proof
                  search have emerged in that area of research, the most prominent
                  representatives are generally described by the buzzwords: automated
                  theorem proving, tactical theorem proving and proof planning. Despite
                  their paradigmatic differences, all approaches share a common goal: to
                  find a proof for a given conjecture. In this paper we start with a
                  rational reconstruction of proof search paradigms in the area of proof
                  planning and tactical theorem proving. Guided by similarities between
                  software engineering and proof construction we develop a uniform view
                  that accommodates the various proof search methodologies and eases their
                  comparison. Based on this view, we propose a unified framework that
                  enables the combination of different methodologies for proof
                  construction to take advantage of their individual virtues within
                  specific phases of a proof construction.},
}