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 model 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.

Towards a unified model of search in theorem proving: subgoal-reduction strategies

BONACINA, Maria Paola
2005

Abstract

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 model 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.
Automated theorem proving; search complexity; analysis of; subgoal-reduction strategies; tableau-based strategies; model elimination; marked search-graphs; bounded search spaces; analytic and synthetic strategies
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/300528
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact