Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleTowards a unified model of search in theorem-proving: subgoal-reduction strategies
Author(s) Maria Paola Bonacina
TypeArticle in Journal
AbstractThis 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.
KeywordsAutomated theorem-proving, Subgoal-reduction strategies, Tableau-based strategies, Strategy analysis, Search model
URL http://www.sciencedirect.com/science/article/pii/S0747717104001324
JournalJournal of Symbolic Computation
Pages209 - 255
Translation No
Refereed No