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

Scheda Prodotto di ricerca

Condividi sui principali social network: Facebook    Delicious    add to CiteUlike
Autori:
Maria Paola Bonacina

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

Anno:
2005

Tipologia prodotto:
Articolo in rivista

Tipologia ANVUR:
Articolo su rivista

Nazioni degli autori:
ITALIA

Lingua:
Inglese

Categoria ISI-CRUI:
Computer Science & Engineering

Formato:
A Stampa

Referee:

Nome rivista:
Journal of Symbolic Computation

ISSN Rivista:
0747-7171

N° Volume:
39

Numero o Fascicolo:
2

Editore:
Elsevier

Intervallo pagine:
209-255

Numero di pagine:
47

Pubblicazione ISI:

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

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.

Pagina Web:
http://profs.sci.univr.it/~bonacina

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
Deposito istituzionale Open Access per la diffusione dei contributi derivanti dall'attività di ricerca delle strutture dell'Università di Verona e di enti scientifici ad essa collegati.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: open|archive*ateneo|univr|it <== Sostituire il carattere | con . e il carattere * con @ per avere indirizzo email corretto.
ornamento
Inizio pagina