کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10325760 | 676805 | 2005 | 47 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Towards a unified model of search in theorem-proving: subgoal-reduction strategies Towards a unified model of search in theorem-proving: subgoal-reduction strategies](/preview/png/10325760.png)
چکیده انگلیسی
This paper advances the design of a unified model for the representation of search in first-order clausal theorem-proving, by extending to tableau-based subgoal-reduction strategies (e.g., model-elimination tableaux), the marked search-graph model, already introduced for ordering-based strategies, those that use (ordered) resolution, paramodulation/superposition, simplification, and subsumption. The resulting analytic marked search-graphs subsume AND-OR graphs, and allow us to represent those dynamic components, such as backtracking and instantiation of rigid variables, that have long been an obstacle to modelling subgoal-reduction strategies properly. The second part of the paper develops for analytic marked search-graphs the bounded search spaces approach to the analysis of infinite search spaces. We analyze how tableau inferences and backtracking affect the bounded search spaces during a derivation. Then, we apply this analysis to measure the effects of regularity and lemmatization by folding-up on search complexity, by comparing the bounded search spaces of strategies with and without these features. We conclude with a discussion comparing the marked search-graphs for tableaux, linear resolution, and ordering-based strategies, showing how this search model applies across these classes of strategies.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 39, Issue 2, February 2005, Pages 209-255
Journal: Journal of Symbolic Computation - Volume 39, Issue 2, February 2005, Pages 209-255
نویسندگان
Maria Paola Bonacina,