Towards a Framework to Integrate Proof Search Paradigms. Autexier, S., Benzmüller, C., & Hutter, D. Technical Report SR-03-02, Saarland University, SEKI Publications (ISSN 1437-4447), 2003. ![Towards a Framework to Integrate Proof Search Paradigms [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Preprint abstract bibtex 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.
@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},
url_preprint = {http://christoph-benzmueller.de/papers/R21.pdf},
Year = 2003,
}
Downloads: 0
{"_id":"LpzfuAy6J5WBugznc","bibbaseid":"autexier-benzmller-hutter-towardsaframeworktointegrateproofsearchparadigms-2003","author_short":["Autexier, S.","Benzmüller, C.","Hutter, D."],"bibdata":{"bibtype":"techreport","type":"SEKI Report","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":[{"firstnames":["Serge"],"propositions":[],"lastnames":["Autexier"],"suffixes":[]},{"firstnames":["Christoph"],"propositions":[],"lastnames":["Benzmüller"],"suffixes":[]},{"firstnames":["Dieter"],"propositions":[],"lastnames":["Hutter"],"suffixes":[]}],"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","url_preprint":"http://christoph-benzmueller.de/papers/R21.pdf","year":"2003","bibtex":"@techreport{R21,\n Abstract =\t {Research on automated and interactive theorem\n proving aims at the mechanization of logical\n reasoning. Aside from the development of logic\n calculi it became rapidly apparent that the\n organization of proof search on top of the calculi\n is an essential task in the design of powerful\n theorem proving systems. Different paradigms of how\n to organize proof search have emerged in that area\n of research, the most prominent representatives are\n generally described by the buzzwords: automated\n theorem proving, tactical theorem proving and proof\n planning. Despite their paradigmatic differences,\n all approaches share a common goal: to find a proof\n for a given conjecture. In this paper we start with\n a rational reconstruction of proof search paradigms\n in the area of proof planning and tactical theorem\n proving. Guided by similarities between software\n engineering and proof construction we develop a\n uniform view that accommodates the various proof\n search methodologies and eases their\n comparison. Based on this view, we propose a unified\n framework that enables the combination of different\n methodologies for proof construction to take\n advantage of their individual virtues within\n specific phases of a proof construction.},\n Author =\t {Serge Autexier and Christoph Benzm{\\\"u}ller and\n Dieter Hutter},\n Institution =\t {Saarland University, SEKI Publications (ISSN\n 1437-4447)},\n Number =\t {SR-03-02},\n Publisher =\t {SEKI Publications (ISSN 1437-4447)},\n Title =\t {Towards a Framework to Integrate Proof Search\n Paradigms},\n Type =\t {SEKI Report},\n url_preprint = {http://christoph-benzmueller.de/papers/R21.pdf},\n Year =\t 2003,\n}\n\n","author_short":["Autexier, S.","Benzmüller, C.","Hutter, D."],"key":"R21","id":"R21","bibbaseid":"autexier-benzmller-hutter-towardsaframeworktointegrateproofsearchparadigms-2003","role":"author","urls":{" preprint":"http://christoph-benzmueller.de/papers/R21.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"techreport","biburl":"http://page.mi.fu-berlin.de/cbenzmueller/papers/chris.bib","dataSources":["ckRabafyoGpACyPpf","S5G7BggtbXZA2Q63T"],"keywords":[],"search_terms":["towards","framework","integrate","proof","search","paradigms","autexier","benzmüller","hutter"],"title":"Towards a Framework to Integrate Proof Search Paradigms","year":2003}