Modello interattivo per la valutzione di insiemi di espressioni predicative

• Autore: Enrico Maretti
• Carica: Ricercatore del CNR
• Pagine: 55-73

Page 55

Enrico Maretti é coordinatore del Grtippo scientifico per l'Informatica della Regione Lombardia.

Le procedure ed i programmi qui illustrati, sono stati utilizzati per esemplificare derivazioni tanto nel campo della logica delle proposizioni inanalizzate (v. A. Gallizia e E. Maretti, Un algoritmo di valutazione per insiemi di Proposizioni inanalizzate, in «Informatica e diritto», IH [1977], 2, pp, 281 ss.) quanto nel calcolo predicativo, apparse a titolo di commento sperimentale nel tomo primo del volume monografico Logica, informatica, diritto, (a cura di A, A, Martino, E. Maretti, C. Ciam-pi), in «Informatica e diritto», JV [1978], 2 pp, 36 ss.).

Poiché il sistema CRONUS è in via di evoluzione, si allega la descrizione sintetica della versione corrente quale appare nella variabile globale DESCRIBE della librerìa pubblica CRONUS utilizzabile dagli utenti della rete I. P. SHARP APL. Utilizzando il comando di sistema )LOAD 610 CRONUS una volta attivato lo spazio operativo sono disponibili due modalità d'uso:

- di utilizzazione diretta del sistema,

- di utilizzazione indiretta delle funzioni costitutive del sistema.

La prima modalità riguarda l'utilizzatore non interessato al linguaggio APL ma ai soli risultati forniti dal sistema; la funzione principale CONSIST attiva le procedure previste mediante un insieme -di semplici comandi interattivi; la seconda. richiede la conoscenza di APL per ricomporre le funzioni base in forma diversa dall'originale od anche mutando le funzioni stesse od integrandole con nuove funzioni definite dalfutilizzatore: per tale motivo tutte le funzioni sono libere e modificabili.

Data di redazione dell'articolo: 29,12,1977.

1. CRONUS: precisazioni su un progetto

1.1. Il sistema CRONUS nasce come controparte strumentale di una ricerca in corso su questioni di logica e di linguistica. I motivi che mi hanno sollecitato a ripensare e redigere un complesso di programmi attinenti, lato sensu, alla logica, sono eminentemente pragmatici: le difficoltà di usare i sistemi esistenti (in verità non molto numerosi) e le loro scarse doti di modificabilità ed estendibilità.

La formulazione in APL contribuisce in modo essenziale ad assicurare al sistema un elevato grado di flessibilità per la possibilità di frammentare le procedure in funzioni base, variamente componibili. Ciò permette,Page 56 fra l'altro, la tacile ricomposizione In sotto-procedure, dedicate a problemi non direttamente pertinenti allo scopo primario- del sistema, come è il caso dell'applicazione qui descritta: chiaramente questo allargamento dell'ambito di utilizzazione acquista maggior generalità se tali estensioni non presentino alcune difficoltà di esercizio per gli utilizzatoti non interessati ai risvolti informatici.

Fra le utilizzazioni secondarie cito:

- la verifica di deducibilità;

- la sperimentazione didattica. .

1.2. La procedura qui presentata (CRONUS-2) svolge la verifica di deducibilità della conclusione da un insieme, anche vuoto, di premesse, nell'ambito del calcolo predicativo del primo ordine. Essa è un'estensione di un'analoga procedura (v. Gallizia- e Maretti, 1977) valida nell'ambito della logica delle proposizioni inanalizzate.

Queste due procedure (CRONOS 1 e 2) hanno come punto di somiglianzà il metodo' di verifica (metodo- degli alberi semantici) e possono situarsi lungo una sola linea di sviluppo, che gradualmente approfondisce il suo grado di analiticità nella descrizione della lingua naturale da cui derivano le espressioni legali del sistema; entrambe fanno parte del -progetto CRONUS, in cui sono previsti (ed in parte sviluppati) altri strumenti, che pur appartenendo- ti dominio della logica, sono basati su princìpi diversi.

1.3, L'inserimento in-un progetto, volto essenzialmente a questioni di logica, di costruzioni parziali, quali appunto CRONUS 1 e 2, dedicati ad applicazioni esterne alla logica, non risponde soltanto ad esigenze di ve-rifiche sperimentali sulla correttezza ed efficienza concreta degli algoritmi, ma anche al tentatilo di rispondere al noto problema della sterilità della logica ricorrente nqn solo nello strascicato tramonto- dell'aristotelismo ma anche neìla primavera della logica moderna. Di questi momenti di malessere sono ben avvertiti i logici più profondamente impegnati nelle situzioni problematiche e non appagati dalla sterminata produzione' rigoristica-scritterale (a cui invero l'informatica contribuisce pesantemente). A questo proposito mi ritorna spesso alla mente il paragone dei tentativi di formalizzare certe zone problematiche dell'attività intellettuale con fuso dell'aereo per visitare un amico abitante nella stessa città: questa immagine non può venir disinvoltamente relegata nel limbo dell'ironia ma ' attentamente valutata, in quanto non pronunciata da un cultore di metafisica ma da un logico sottile come Hao Wang.

Il diritto offre un campo dIndagine' emblematico1, in posizione mediana fra la matematica, dove vigono le strutture numeriche e seriali della quantità, ed immondo delle lettere in cui il libero gioco delle categorie semantiche rifugge dalla regolarità, CRONUS-2 non vuol essere un tentativo di mediazione teorica ma soltanto- un modestissimo strumento'per affron-Page 57 tare situazioni logiche molto semplici del calcolo predicativo del primo ordine, ma già maggiormente aderenti ai modi consueti della verbalizzi-' zione giuridica di quanto non sia il calcolo delle proposizioni inanalizzate (CRONUS-1), pur rispecchiando lo stesso fine: fornire al giurista mezzi, semplici all'uso, per affrontare calcoli connessi a problemi di deducibilità, delegando all'automa il banale, ma gravoso svolgimento delle dimostrazioni. Si lascia, ad ulteriori sviluppi l'estensioni alle logiche modali più direttamente coinvolgenti il ragionamento giuridico. Credo infatti che strumenti, pur ancora nella fase elementare, possano svolgere un ruolo non secondario sia nell'avvicinare due attività, il diritto e la logica, aecor molto lontane nella prassi quotidiana, sia nel suggerire spunti verso nuove direzioni di ricerca: in questo senso si può parlare di mediazione pragmatica. Infatti, il peso dei passaggi di tipo « calcolistico » allontana gli usi della logica anche nei casi in cui 'un aiuto (ancorché modesto) essa potrebbe dare al chiarimento di situazioni giuridiche complesse. Sono ben lungi dal pensare ad un « calcolo » in senso leibniziano risolutore dei casi problematici' del diritto, ma più semplicemente ad un avvio fondato- non solo su prerequisiti teoretici ma anche suggerito dalla concretezza dei casi. I limiti di questo strumento fondato sulla logica dal primo ordine sono molto severi, più che per l'assenza delle modalità (su cui fra l'altro insistono ancora molte ombre) per l'impossibilità di ricorrere a variabili predica rive e quindi « calcolare », secondo- il suggerimento- di Taine con « qua-Mtà imperfettamente rilevate e imperfettamente codificate ». Comunque pur nel suo ristretto orizzonte questo ulteriore passo « meccanico », se valutato nel suo ambito di apporto tecnico potrebbe contribuire alla delimitazione della zona dagli incerti confini ove si scambiano- i modi della logica e dell Intuizione.

Con tutti i limiti e le cautele imposti da uno strumento che, pur agevolando i passaggi calcolabili, porta con sé le incertezze delle strutture logiche, si può ipotizzare, al di là, appunto dello- sveltimento dei calcoli, sia una maggior penetrazione delle argomentazioni giuridiche, se non altro per lo sforzo implicato dalla funzione parafrastica, sia possibili spunti innovativi diretti ad ampliare o approfondire o rifonnulare settori della logica nonché, subordinatamente, le componenti informatiche.

@2. Gli alberi semantici

'Ogni proposizione è vera o falsa; ma non entrambe ' Gran parte della lcfgica consiste in uno sviluppo pedissequo di questa banalità

.

(R. C, Jeffey, Formai Logic)

2.1. Il metodo degli alberi semantici, su cui si fonda II presente algoritmo (v. Gallizia e Maretti, 1976) è stato proposto modernamente da Jeffrey (Jeffrey, 1977) come semplificazione delle tavole semantiche utilizzate da Beth (Beth, 19.59) quale strumento scritturale (tipografico) per la « ri-Page 52 cerca di controesempi in modo sistematico »: come è noto la prova per contraddizione risale ad Aristotele, ove, però manca la sistematicità, almeno in parte adombrata nella discussa dimostrazione per ekihesis. Sotto altro angolo visuale le tavole semantiche si configurano come risultato di una mediazione fra due atteggiamenti opposti dei logici, del privilegio delle forme sul contenuto, o del contenuto sulla forma, in termini più alla moda visualizzabili nel binomio-cesura sintassi/semantica» Mentre le tavole semantiche si sviluppano in successive partizioni (i quadranti del vero e del falso) gli alberi di Jeffrey semplificano- notevolmente il problema sviluppandone un solo lato: le due procedure si equivalgono nei risultati causa Fuso della negazione nelle regole di frammentazione delle espressioni. Una chiara esposizione del metodo si trova in Beth (1959, 1970) e ve abbondano i richiami storici e le motivazioni filosofiche e logiche, mentre nei volumi di Jeffrey (1967) e Le'blanc (1972) viene accentuato-l'aspetto costruttivo' (se si vuole « meccanico ») del...