Towards a Framework to Integrate Proof Search Paradigms (bibtex)
by Serge Autexier, Christoph Benzmüller, Dieter Hutter
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.
Reference:
Towards a Framework to Integrate Proof Search Paradigms (Serge Autexier, Christoph Benzmüller, Dieter Hutter), SEKI Publications (ISSN 1437-4447), number SR-03-02, 2003. (Url (preprint): http://christoph-benzmueller.de/papers/R21.pdf)
Bibtex Entry:
@techreport{R21,
  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.},
  Author =	 {Serge Autexier and Christoph Benzm{\"u}ller and
                  Dieter Hutter},
  Institution =	 {Saarland University, SEKI Publications (ISSN
                  1437-4447)},
  Number =	 {SR-03-02},
  Publisher =	 {SEKI Publications (ISSN 1437-4447)},
  Title =	 {Towards a Framework to Integrate Proof Search
                  Paradigms},
  Type =	 {SEKI Report},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/R21.pdf}},
  Year =	 2003,
}
Powered by bibtexbrowser