In questo lavoro sono riportati i risultati finora ottenuti nel progetto di un dimosrratore di teoremi parallelo che utilizza un calcolo in deduzione naturale. La gestione a runtime del parallelismo è un problema della massima importanza nella parallelizzazione di un programma ed il modello a sponsorizzazione appare essere adeguato come possibile approccio per la schedulazione di processi paralleli. Una analisi di fattibilità in merito alla scelta di eseguire in parallelo le strategie alternative di prova attivate dal dimostartore è stata necessaria per determinare la granularità dei processi ed i costi oomputazionali connessi alla loro creazione ed esecuzione.
Un Dimostratore di Teoremi Parallelo in Deduzione Naturale
A Calabrese
1992
Abstract
In questo lavoro sono riportati i risultati finora ottenuti nel progetto di un dimosrratore di teoremi parallelo che utilizza un calcolo in deduzione naturale. La gestione a runtime del parallelismo è un problema della massima importanza nella parallelizzazione di un programma ed il modello a sponsorizzazione appare essere adeguato come possibile approccio per la schedulazione di processi paralleli. Una analisi di fattibilità in merito alla scelta di eseguire in parallelo le strategie alternative di prova attivate dal dimostartore è stata necessaria per determinare la granularità dei processi ed i costi oomputazionali connessi alla loro creazione ed esecuzione.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
