Informatica e diritto, III Annata, Vol. III, 1977, n. 2, pp. 281-336

Enrico Maretti, Angelo Gallizia

Un algoritmo di valutazione per insiemi di proposizioni inanalizzate

Il lavoro presentato nell'articolo s'inquadra in un'indagine volta a verificare la possibilitā di affidare all'elaboratore elettronico l'esecuzione di procedure logiche di possibile utilizzazione immediata. Come primo passo viene affrontato il calcolo delle proposizioni inanalizzate (o calcolo degli enunciati), premessa al calcolo dei predicati del primo ordine, delle modalitā e delle logiche non classiche. L'algoritmo proposto, per la valutazione di consistenza (o inconsistenza) in insiemi di espressioni proposizionali, si ispira allo schema degli alberi di derivazione, a sua volta risultante dalla modificazione apportata da Smullyan alle tavole semantiche introdotte da Beth.
Sulla base dei richiami ai metodi delle tavole semantiche e degli alberi di derivazione viene descritto il programma elaborato: questo č in grado di svolgere a richiesta un numero a piacere di derivazioni e ogni derivazione viene articolata in due fasi, consistenti rispettivamente nella immissione dell'insieme di espressioni (una alla volta) e nella costruzione dell'albero di consistenza con la relativa stampa dei risultati. Vengono descritte le singole funzioni del programma e precisati il carattere (di semplice strumento di ricerca) e i limiti (soprattutto nei tempi di esecuzione) dello stesso; in particolare, sono chiariti, poi, il valore e il senso dell'applicazione della procedura degli alberi di consistenza alle situazioni giuridiche.
Concludono l'articolo, dopo un richiamo all'opportunitā di esplorare i risvolti applicativi della logica moderna, due Appendici che riportano, la prima, alcuni cenni relativi alla documentazione del programma e, la seconda,  lo svolgimento di brevi sessioni di lavoro e l'illustrazione di alcuni esempi di derivazioni.

vai al testo integrale / see full text