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

Scheda Prodotto di ricerca

Condividi sui principali social network:

Autori:: Maria Paola Bonacina
Titolo:: Towards a unified model of search in theorem proving: subgoal-reduction strategies
Anno:: 2005
Breve descrizione dei contenuti:: 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.
Nome rivista:: Journal of Symbolic Computation
ISSN:: 0747-7171
Editore:: Elsevier
Tipologia prodotto:: Articolo in rivista
Tipologia ANVUR:: Articolo su rivista
Categoria ISI-CRUI:: Computer Science & Engineering
Lingua:: Inglese
Nazioni degli autori:: ITALIA
Formato:: A Stampa
Pubblicazione ISI:: Sì
Numero di pagine:: 47
Intervallo pagine:: 209-255
Parole chiave:: 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
Pagina Web:: http://profs.sci.univr.it/~bonacina
Referee:: Sì
N° Volume:: 39
Numero o Fascicolo:: 2
Id prodotto:: 20899
Id Ugov:: 300528
depositato da:: Maria Paola Bonacina
depositato il:: 15 marzo 2012
ultima modifica:: 15 marzo 2012

Progetti Collegati
Titolo	Dipartimento	Responsabili
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003)	Dipartimento Informatica	Maria Paola Bonacina

<<indietro
Il presente archivio pubblico di Ateneo, sviluppato dall'Università di Verona e integrato con il gestore dei prodotti della ricerca U-gov Cineca, realizza un sistema di Open Archive ed assicura l'interoperabilità dei metadati conformemente allo standard Open Archives Protocol for Metadata Harvesting OAI 2.0. Per contattare l'amministratore dell'archivio scrivere a: openarchiveateneounivrit