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
An Evaluation Algorithm for Sets of not Analyzed Propositions
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 Smullvan 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, seconda, lo svolgimento di brevi sessioni di lavoro e l'illustrazione di alcuni esempi di derivazioni.
The article reports on a work carried out for a research aiming at testing the possibility of automatically processed logic procedures immediately employable. First of all the Authors analyze the calculus of not analyzed propositions (or propositional calculus), as an introduction to the calculus of first order predicates, of modalities and of not classical logic. The algorithm proposed to evaluate the consistency (or non consistency) of propositional sets, is based on the scheme of the derivation tree, deriving from the changes carried out by Smullyan to the semantic tables introduced by Beth. The Authors describe the program based on the methods of semantic table and of derivation trees: the program can carry out, request, a number of derivations and every derivation can be divided into two is, the input of propositional sets (one by one) and the construction of the consistency tree, followed by the printing of results. The Authors describe the different functions of the program, precise its nature of a simple research instrument., its limits, of execution in particular, and the importance and the meaning of the procedure of the consistency tree applied to law. After pointing out the necessity to investigate the possible of modern logic, the Authors enclose two Appendixes, the first on the program documentation, and the second on short work sessions and some derivation examples.