LOGICA E INFORMATICA

LOGICA E INFORMATICA

I. McCarthy (1963) afferma che è ragionevole sperare che le relazioni tra l'i. e la l. matematica nel prossimo secolo saranno altrettanto fruttuose di quelle tra l'analisi e la fisica nel secolo scorso. È troppo presto per valutare questa previsione di McCarthy. Ciò non impedisce di chiedersi se, negli sviluppi dell'i. dalle origini fino a oggi, esistano segni che incoraggino tali speranze. Questi segni in effetti esistono e riguardano principalmente cinque aree: la macchina a registri illimitati, il λ−calcolo, la programmazione logica, l'uso della l. come linguaggio di programmazione e la sintesi logica dei programmi.

La macchina a registri illimitati. − Nell'ambito del suo programma fondazionale, D. Hilbert aveva ripetutamente ribadito la convinzione che ogni problema matematico potesse essere risolto mediante un numero finito di operazioni. Tale convinzione venne confutata da un risultato di A. Turing (1937). Per ottenere tale risultato Turing ideò un modello puramente matematico dei procedimenti di computo sotto forma di una macchina ideale capace di manipolare simboli, comunemente nota come macchina di Turing. Successivamente sono stati formulati modelli più adeguati, per es. la macchina a registri illimitati di J.C. Shepherdson e H.E. Sturgis (1963).

La macchina a registri illimitati consta di una casella R₀, detta contatore di programma, e di una successione (potenzialmente) infinita di caselle R₁, R₂, R₃,... dette registri. A ogni passo del computo il contatore di programma e i registri contengono un numero naturale. Indichiamo con r_i il numero naturale contenuto in R_i.

I contenuti del contatore di programma e dei registri possono essere modificati dalla macchina in risposta a certe istruzioni di tipo molto elementare fissato. Una successione finita di istruzioni I₁,...,I_n si dice un programma.

Le istruzioni sono di una delle seguenti forme:

1) per ogni n>0 c'è un'istruzione zero: Z_n. In risposta a questa istruzione la macchina scrive 0 in R_n e aumenta di 1 il contenuto di R₀ lasciando inalterati i contenuti degli altri registri;

2) per ogni n>0 c'è un'istruzione successore: S_n. In risposta a tale istruzione la macchina aumenta di 1 il contenuto di R_n e di R₀ lasciando inalterati i contenuti degli altri registri;

3) per ogni n, m>0 c'è un'istruzione di trasferimento: T_{n, m}. In risposta a tale istruzione la macchina trasferisce il contenuto di R_n in R_m (cioè pone il numero naturale r_n in R_m) e aumenta di 1 il contenuto di R₀ lasciando inalterati i contenuti di tutti gli altri registri;

4) per ogni n, m, k>0 c'è un'istruzione di salto: J_{n, m, k}. In risposta a tale istruzione la macchina confronta i contenuti di R_n ed R_m lasciando inalterati i contenuti di tutti i registri. Se r_n=r_m, allora la macchina mette il numero naturale k in R₀. Se r_n≠r_m, allora la macchina aumenta di 1 il contenuto di R₀;

5) c'è infine un'istruzione di fermata: Stop. In risposta a tale istruzione la macchina si ferma.

Per il funzionamento della macchina a registri illimitati occorre che:

a) sia dato un programma I₁,...,I_h, dove I_h è l'istruzione di fermata Stop;

b) sia data una configurazione iniziale dei registri, cioè una successione di numeri naturali q₁, q₂, q₃,... nei registri R₁, R₂, R₃,... rispettivamente;

c) il contenuto iniziale del contatore di programma R₀ sia 1. Il contenuto di R₀ indica il numero della prossima istruzione eseguita dalla macchina. Questa comincia con l'eseguire l'istruzione I₁. Supponiamo che la macchina abbia eseguito l'istruzione I_i, 1≤i〈h. Se I_i non è un'istruzione di salto J_{n, m, k}, allora l'istruzione successiva eseguita è I_i+1. Se invece lo è, allora la prossima istruzione eseguita dalla macchina è I_i+1 se r_n≠r_m, mentre è I_k se r_n=r_m (dove si suppone che 1≤k≤h). La macchina continua a eseguire istruzioni del programma I₁,...,I_h fino a che in R₀ viene posto il numero h. Poiché I_h è un'istruzione di fermata, allora la macchina si ferma. La configurazione finale dei registri, cioè la successione r₁, r₂, r₃,... dei contenuti di R₁, R₂, R₃,... quando la macchina si ferma, costituisce il risultato finale dell'esecuzione del programma I₁,...,I_h con la configurazione iniziale dei registri q₁, q₂, q₃,...

Per es. supponiamo di voler scrivere un programma per sommare due numeri naturali n ed m: la somma n+m si può ottenere aumentando di 1 il numero n un numero m di volte. Come configurazione iniziale dei registri prendiamo n, m, 0, 0, 0,... (cioè n in R₁, m in R₂ e 0 in tutti gli altri registri). Il programma deve far sì che la macchina continui ad aumentare di 1 il contenuto di R₁, usando R₃ come contatore per contare quante volte tale contenuto è stato aumentato di 1, e si fermi con configurazione finale dei registri n+m, 0, 0, 0,... (cioè n+m in R₁ e 0 in tutti gli altri registri). Un programma con queste caratteristiche è il seguente:

Si noti che in risposta a I₄ la macchina salta sempre indietro a I₁. Per es., se si calcola 3+2 con tale programma, il contenuto del contatore di programma e dei registri dopo ciascuna istruzione è:

Esiste una corrispondenza piuttosto stretta tra la macchina a registri illimitati e i calcolatori attuali. La macchina con la sua capacità di rispondere alle istruzioni corrisponde all'unità centrale del calcolatore, le istruzioni corrispondono alle macroistruzioni dell'unità centrale, e i registri corrispondono alle locazioni di memoria del calcolatore. La differenza più rilevante sta nel fatto che nella macchina a registri illimitati il programma non risiede nei registri, quindi non può modificare se stesso nel corso dell'esecuzione. Si può, però, modificare la nozione di macchina a registri illimitati in modo da incorporare questa caratteristica (macchina a programma memorizzato).

Tuttavia, rispetto alla macchina a registri illimitati, i calcolatori attuali presentano alcune sostanziali limitazioni:

1) il numero delle locazioni di memoria di un calcolatore è limitato, mentre quello dei registri della macchina a registri illimitati è (potenzialmente) infinito;

2) le singole locazioni di memoria di un calcolatore possono contenere solo numeri di grandezza limitata, mentre ciascun registro della macchina a registri illimitati può contenere numeri comunque grandi;

3) la complessità dei programmi di un calcolatore è limitata dal tempo di esecuzione, mentre una macchina a registri illimitati può eseguire programmi di complessità qualsiasi.

Tali limiti, però, non sono fissati una volta per tutte, e l'evoluzione tecnologica tende continuamente a spostarli in avanti. In questo senso la macchina a registri illimitati costituisce una soddisfacente idealizzazione del funzionamento dei calcolatori attuali.

Il λ−calcolo. - Un modello matematico alternativo dei procedimenti di computo venne introdotto da A. Church (1932) attraverso il suo λ−calcolo. Mentre la macchina a registri illimitati fornisce una modellizzazione a basso livello (cioè a livello del linguaggio-macchina) dei calcolatori attuali, il λ-calcolo fornisce una modellizzazione a un più alto livello dei procedimenti di computo.

Consideriamo l'espressione x-y. Essa può essere intesa come definente una funzione f di x, cioè f:x→x-y, oppure una funzione g di y, cioè g:y→x-y, oppure una funzione h di x e y, cioè h:x, y→x-y. Church introdusse un modo sistematico per distinguere tra questi vari modi d'intendere la stessa espressione usando il simbolo λ. Usando tale simbolo le funzioni precedenti possono essere scritte: f:λx·x-y, g: λy·x-y, h: λxy·x-y. Per es. le equazioni f(1)=1−y, g(0)=x-0, h(1, 0)=1-0 in λ−notazione diventano (λx·x-y) (1)=1−y, (λy·x-y) (0)=x-0, (λxy·x-y) (1, 0)=1-0.

La λ−notazione è apparentemente goffa, ma non bisogna lasciarsi ingannare dalle apparenze: il suo scopo principale è quello di denotare funzioni di ordine superiore, cioè funzioni i cui valori non sono numeri bensì altre funzioni. In effetti, contrariamente a quanto abbiamo fatto sopra per la funzione h, non è necessario introdurre una speciale notazione, nella fattispecie λxy·x-y, per le funzioni di più variabili: è sufficiente usare funzioni i cui valori sono altre funzioni. Così, invece di h, si può considerare la funzione h⁺ di x definita da: h+=λx·(λy·x-y). Per ogni numero a si ha h+(a)=λy·a-y, per cui per ogni coppia di numeri a, b si ha (h+(a)) (b)=(λy·a-y) (b)=a-b=h(a, b). Perciò h+ ''rappresenta'' h. Per questo motivo si può evitare di considerare funzioni di più variabili, limitandosi alle sole funzioni di una variabile.

Queste nozioni informali sulla λ−notazione possono essere formulate sistematicamente sotto forma di un sistema formale, il λ−calcolo. Per costruirlo supponiamo data una successione infinita di simboli distinti detti variabili, e una successione finita o infinita di simboli distinti detti costanti. L'insieme delle espressioni dette λ−termini è definito induttivamente nel modo seguente: a) tutte le variabili e le costanti sono λ−termini; b) se M ed N sono λ−termini, allora (MN) è un λ−termine; c) se M è un λ−termine e x è una variabile, allora (λx·M) è un λ−termine. Nello scrivere i λ−termini le parentesi possono essere omesse secondo la convenzione dell'associatività a sinistra, per cui per es. MNP denota ((MN)P). Inoltre si può scrivere λx·MN per (λx·(MN)).

L'interpretazione dei λ−termini è la seguente. Le variabili rappresentano funzioni qualsiasi (di una variabile). (MN) rappresenta il risultato dell'applicazione della funzione M all'argomento N. (λx·M) rappresenta la funzione il cui valore per l'argomento N è il risultato della sostituzione di x con N in M. Per es. λx·x(xy) rappresenta l'operazione di applicare una funzione due volte a un particolare argomento y, sicché per tutti i termini N l'equazione (λx·x(xy))N=N(Ny) vale nel senso che entrambi i lati dell'equazione hanno la stessa interpretazione.

Si può definire un procedimento formale di computo con i λtermini che segue da vicino la loro interpretazione. Ma per farlo occorre definire anzitutto l'operazione di sostituzione di una variabile con un termine (che è stata usata sopra informalmente).

Un'occorrenza di una variabile x in un termine P si dice vincolata se è in una parte di P della forma λx·M; altrimenti si dice libera. Se x ha almeno un'occorrenza libera in P, si dice che x è una variabile libera di P. L'insieme delle variabili libere di P si indica con VL(P).

Il risultato [N/x] M della sostituzione di ogni occorrenza libera di x in M con N (cambiando le variabili vincolate per evitare conflitti di variabili) è definito induttivamente nel modo seguente: 1) [N/x] x=N; 2) [N/x] a=a se a è una variabile o costante diversa da x; 3) [N/x] (PQ)=([N/x]P) ([N/x] Q); 4) [N/x] (λx ·P)=λx ·P; 5) [N/x] (λy ·P)=λy ·[N/x] P se y≠x, e y∉ VL(N) oppure x ∉ VL (P); 6) [N/x] (λy·P)=λz·[N/x] [z/y] P se y≠x e y ∉ VL(N) e x ∉ VL(P) e z è la prima variabile ∉ VL(NP). La clausola (f) di questa definizione fa sì che il significato intuitivo di [N/x] (λy ·P) non dipenda dalla scelta della variabile vincolata y.

Se P è un termine contenente un'occorrenza di λx ·M, e y ∉ VL(M), l'atto di rimpiazzare tale occorrenza di λx·M con λy·[y/x] M si dice un cambio di variabile vincolata in P. Si dice che P è congruente con Q, o che P si α−converte in Q, se Q si ottiene da P con un numero finito (anche vuoto) di cambi di variabili vincolate. Termini congruenti hanno interpretazioni identiche e svolgono ruoli identici in tutte le applicazioni del λ−calcolo.

In base all'interpretazione dei λ−termini un termine della forma (λx ·M)N rappresenta il risultato dell'applicazione della funzione λx ·M all'argomento N. Ancora in base all'interpretazione dei λ−termini il valore della funzione λx ·M per l'argomento N viene calcolato sostituendo x con N in M, sicché (λx ·M)N può essere ''computato'' come [N/x] M.

Questo processo di computo è inglobato nella seguente definizione: se un termine P contiene un'occorrenza di (λx ·M)N e se Q si ottiene rimpiazzando tale occorrenza con [N/x] M, allora si dice che P si β−contrae in Q; (λx·M)N si dice un β−contraendo e [N/x] M si dice il suo contratto. Se Q si ottiene da P con una successione finita (anche vuota) di β−contrazioni e cambi di variabili vincolate, allora si dice che P si β−riduce a Q, e si scrive P ▷_β Q. Per es. (λx·x(xy))N ▷_β N(Ny), (λx·(λy·yx)z)v ▷_β zv, e (λx·xx) (λx·xx) ▷_β (λx·xx) (λx·xx). Quest'ultimo esempio mostra che il processo di computo non termina necessariamente. Esso termina solo se dà luogo a un termine non contenente β−contraendi.

Ciò suggerisce la seguente definizione. Un termine Q che non contiene β−contraendi si dice una β−forma normale (o un termine in β-forma normale). Se P ▷_β Q e Q è in β−forma normale, allora si dice che Q è una β−forma normale di P. Per es. zv è una β−forma normale di (λx·(λy·yx)z)v. I termini in β−forma normale sono dei termini ''computati completamente''. La β−forma normale di un termine P costituisce il più semplice termine avente la stessa interpretazione di P.

Alcuni termini possono essere β−ridotti in più modi differenti. Per es. (λx·(λy·yx)z)v si β−contrae sia in (λy·yv)z che in (λx·zx)v. Entrambi questi termini, però, si β−contraggono in zv, quindi entrambe le β−riduzioni conducono alla stessa β−forma normale. Vale questo in generale? Una risposta affermativa è data dal teorema di Church-Rosser (1936): Se P ▷_β M e P ▷_β N, allora esiste un Q tale che M ▷_β Q ed N ▷_β Q.

Si è già detto che il λ−calcolo costituisce una modellizzazione dei procedimenti di computo a un più alto livello della macchina a registri illimitati. In effetti esso ha ispirato la formulazione di un linguaggio di programmazione ad alto livello come il LISP introdotto da McCarthy (1958). Attualmente il λ−calcolo è considerato come un ''banco di prova'' per lo studio di linguaggi di programmazione ad alto livello. Nuove tecniche vengono sviluppate e provate sul λ−calcolo, e poi vengono applicate a linguaggi di programmazione di pratico impiego.

La programmazione logica. − A partire dal 1970 si è venuta affermando una modellizzazione dei procedimenti di computo del tutto diversa dalle precedenti, che identifica i computi con le dimostrazioni formali in un calcolo logico. Ci si riferisce qui alla proposta dovuta essenzialmente a R.A. Kowalski di usare la logica dei predicati come linguaggio di programmazione e come modello di computo. Tale proposta va comunemente sotto il nome di programmazione logica. La programmazione logica può essere considerata come un caso particolare della dimostrazione automatica basata sul metodo di risoluzione introdotto da A. Robinson (1965). Per introdurre i concetti fondamentali di quest'ultima occorre formulare anzitutto la sintassi delle clausole del calcolo dei predicati del primo ordine.

Supponiamo data una successione infinita di simboli distinti detti variabili, e successioni finite o infinite di simboli distinti detti rispettivamente costanti, simboli funzionali e simboli relazionali. L'insieme delle espressioni dette termini è definita induttivamente da: a) tutte le variabili e le costanti sono termini; b) se t₁,...,t_n sono termini ed f è un simbolo funzionale n-ario, allora f(t₁,...,t_n) è un termine. Gli atomi sono le espressioni della forma P(t₁,...,t_n), dove t₁,...,t_n sono termini e P è un simbolo relazionale n-ario. I letterali sono gli atomi e le negazioni ¬A di atomi A. Una clausola è una disgiunzione A₁ ⋁...⋁ A_n di letterali A₁,...,A_n. L'interesse delle clausole deriva dal fatto che esiste un procedimento, detto di skolemizzazione, che permette di tradurre ogni insieme di formule del calcolo dei predicati del primo ordine (contenente quindi in generale dei quantificatori) in un insieme di clausole.

Il metodo di risoluzione è un metodo che permette di stabilire se una clausola è una conseguenza di un insieme di clausole.

Esso si basa sulla regola di inferenza di risoluzione che è definita nel modo seguente. Siano C₁ e C₂ le clausole C₁=A₁ ⋁...⋁ A_n e C₂=B₁ ⋁...⋁ B_m. Se esiste una sostituzione σ delle variabili di C₁ e C₂ con dei termini tale che σ(A_i)=¬σ (B_j) (cioè tale che il risultato della sostituzione in A_i è identico alla negazione del risultato della sostituzione in B_j), allora la clausola C₃=σ(A₁ ⋁...⋁ A_i−1 ⋁ A_j+1 ⋁...⋁ A_n ⋁ B₁ ⋁...⋁ B_j-1 ⋁ B_j+1 ⋁...⋁ B_m) è una conseguenza logica (un risolvente) di C₁ e C₂. Per es. se C₁=¬P(s(0), s(0), w) ⋁¬P(w, s(0), w₁), C₂=¬P(x, y, z) ⋁ P(s(x), y, s(z)) e σ è la sostituzione di x con 0, di y con s(0) e di w con s(z), allora C₃=¬P(s(z), s(0), w₁) ⋁¬P(0, s(0), z) poiché σ(¬P(s(0), s(0), w))=¬σP(s(x), y, s(z)).

Il metodo di risoluzione si basa sulla generazione di tutti i risolventi, ed è dato dal seguente algoritmo. Dato un insieme di clausole Γ₀ ripetere le seguenti due operazioni: 1) sia Γ_i+1 l'unione di Γ_i e dell'insieme di tutti i risolventi delle clausole in Γ_i; 2) se Γ_i+1 contiene la clausola vuota, allora fermarsi, altrimenti ripetere il passo (1). Una clausola C è una conseguenza di un insieme di clausole Γ se l'algoritmo precedente, applicato all'insieme di clausole Γ₀=Γ∪{¬C} , termina. Per es. se Γ consta delle clausole P(0, x, x) e ¬P(x, y, z) ⋁ P(s(x), y, s(z)) e C è la clausola P(s(0), 0, w), allora l'algoritmo dà luogo al seguente albero:

che dimostra che C è una conseguenza di Γ.

Il metodo di risoluzione ha il difetto di essere molto complesso: il numero dei risolventi cresce molto rapidamente perché a ogni passo si devono considerare i risolventi calcolati precedentemente. Per evitare questo difetto conviene considerare invece di clausole qualsiasi solo clausole di una forma particolare, le cosiddette clausole di Horn. Queste sono costituite: a) dalle clausole definite, cioè clausole contenenti solo negazioni tranne una, della forma A ⋁¬B₁ ⋁...⋁¬B_m (m≥0), dove B₁,...,B_m sono atomi; b) dalle clausole negative, cioè clasole contenenti solo negazioni, della forma ¬B₁ ⋁...⋁¬B_m (m≥0). In generale una clausola della forma A₁ ⋁...⋁ A_n ⋁¬B₁ ⋁...⋁¬B_m può essere rappresentata equivalentemente mediante la formula A₁,...,A_nÁB₁,...,B_m che significa: (B₁ e...e B_m) implica (A₁ oppure ... oppure A_n). Nel caso delle clausole di Horn di solito si preferisce questa notazione. In particolare: a) le clausole definite vengono scritte AÁB₁,...,B_m se m≥1, oppure AÁ se m=0; b) le clausole negative vengono scritte ÁB₁,...,B_m se m≥1, oppure Á se m=0.

Per le clausole di Horn esiste un procedimento di risoluzione molto semplice, detto risoluzione SLD (risoluzione lineare per clausole definite con scelta).

Per spiegarlo consideriamo il seguente esempio. Sia Γ l'insieme consistente delle clausole definite: Mortale (x)ÁUomo (x), Uomo (x)ÁFrancese (x), Francese (Pascal), Uomo (Dante), e sia C la clausola: Mortale (y). Per determinare se C è una conseguenza di Γ scriviamo ¬C nella forma della clausola negativaÁMortale (y). Ciascuno dei due alberi seguenti fornisce una risposta affermativa:

Essi stabiliscono che la conclusione Mortale (y) è soddisfatta se si prende y=Dante oppure y=Pascal.

Come mostra questo esempio la risoluzione SLD è data dal seguente algoritmo per determinare se C è una conseguenza di Γ: 1) trovare una sostituzione σ che unifichi (cioè identifichi) un atomo ¬C con la conclusione (=la parte a sinistra diÁ) di una clausola definita di Γ; 2) riscrivere l'atomo scelto insieme alle premesse (=la parte a destra diÁ) della clausola definita in questione, e applicare la sostituzione σ. La risoluzione SLD ha ispirato la formulazione di un linguaggio ad alto livello come il PROLOG introdotto da A. Colmerauer (1973). Attualmente essa costituisce la base di alcuni efficienti sistemi di dimostrazione automatica di teoremi (come quello di Wos, Overbeek e Lusk che ha permesso di scoprire nuovi teoremi in vari campi, dall'algebra booleana ternaria alla teoria dei nodi) nonché di varie estensioni del PROLOG.

La logica come linguaggio di programmazione. − Il metodo di risoluzione costituisce solo una parziale realizzazione dell'idea di usare la l. dei predicati come linguaggio di programmazione e come modello di computo. Questo perché esso si applica solo a insiemi di clausole e non a insiemi di formule qualsiasi. La skolemizzazione non fa parte del metodo ma è presupposta dal metodo. Inoltre il metodo di risoluzione si applica principalmente alla l. classica e può essere trasportato in altri contesti solo con notevole sforzo, in parte perché i teoremi di forma normale non valgono in generale per le l. non-classiche. Un metodo alternativo a quello di risoluzione è il metodo dei tableaux introdotto da D. Prawitz (1960) sviluppando un metodo precedente di E. Beth (1955). Esso si applica a insiemi di formule qualsiasi e ha naturali estensioni che coprono varie l. non-classiche.

Termini e atomi sono definiti come nel metodo di risoluzione. L'insieme delle espressioni dette formule è definito induttivamente da: a) tutti gli atomi sono formule; b) se A e B sono formule, tali sono anche ¬A, A→B, A⋁B, A→B; c) se A è una formula e x una variabile, allora tali sono anche ∀xA e ∃xA. Le formule segnate sono espressioni della forma TA o FA dove A è una formula. L'interpretazione di TA è: A è vera, quella di FA è: A è falsa. Le formule segnate TA e FA per A non un atomo possono essere raggruppate in cinque categorie: formule negative, congiuntive (o α−formule), disgiuntive (o β−formule), universali (o Γ−formule) ed esistenziali (o δ−formule). Le formule negative hanno un solo componente, le α−formule hanno due componenti indicati con α₁ e α₂, le β−formule hanno due componenti indicati con β₁ e β₂, le Γ−formule hanno un esempio Γ(t) per ogni termine t e le δ−formule hanno un esempio δ(t) per ogni termine t. Le categorie, i componenti e gli esempi sono definiti dalle seguenti tavole:

Il significato delle tavole è il seguente: a) una negativa è vera se e solo se la positiva corrispondente è falsa; b) una α−formula è vera se e solo se entrambi i componenti α₁ e α₂ sono veri: c) una β−formula è vera se e solo se almeno uno dei componenti β₁ e β₂ è vero; d) una Γ−formula è vera se e solo se ogni esempio Γ(t) è vero; e) una δ−formula è vera se e solo se qualche esempio δ(t) è vero.

Come il metodo di risoluzione, anche il metodo dei tableaux può essere descritto in termini di alberi. Supponiamo di voler determinare se C è una conseguenza di Γ={C₁,...,C_n} dove C, C₁,...,C_n sono qualsiasi. L'albero allora comincerà con un ramo costituito dalle formule segnate TC₁,...,TC_n, FC (cioè si suppone che C₁,...,C_n siano vere e C sia falsa). Quindi l'albero proseguirà in base alle seguenti cinque regole:

Se una negativa occorre in un ramo dell'albero, allora il ramo può essere esteso aggiungendo la positiva corrispondente alla fine. Se una α−formula occorre in un ramo, allora il ramo può essere esteso aggiungendo α₁ e α₂ alla fine. Se una β−formula occorre in un ramo, allora il ramo può essere scisso in due rami, uno dei quali si ottiene aggiungendo β₁ e l'altro aggiungendo β₂. Se una Γ−formula occorre in un ramo, allora il ramo può essere esteso aggiungendo Γ(t) alla fine per un termine qualsiasi t senza variabili. Se una δ−formula occorre in un ramo, allora il ramo può essere esteso aggiungendo δ(y) alla fine dove y è una nuova variabile, cioè una variabile che non occorre già nel ramo. Un ramo si dice chiuso se contiene sia TA che FA per qualche formula A. L'albero si dice chiuso se tutti i suoi rami sono chiusi. Se un albero costruito secondo le regole sopra indicate è chiuso, allora si può concludere che C è una conseguenza di Γ. L'esistenza di un albero chiuso significa che l'ipotesi che tutte le formule di Γ siano vere e che C sia falsa conduce a una situazione impossibile, dunque anche C dev'essere vera.

Occorre fare alcune osservazioni a proposito della costruzione dell'albero. Le regole per la generazione dell'albero sono intrinsecamente non-deterministiche. Si può scegliere quale ramo estendere e su quale formula operare senza alcun ordine prefissato. Tuttavia la costruzione dell'albero può essere resa deterministica fissando un ordine nella scelta dei rami da estendere e delle formule su cui operare che sia adeguato, cioè tale che alla fine a ogni formula negativa, α−formula, β−formula o γ−formula occorrente su un ramo sia applicata la regola appropriata, e a ogni δ−formula occorrente su un ramo sia applicata la regola corrispondente usando come termine t tutti i termini del linguaggio non contenenti variabili.

Un ordine adeguato suggerito da R.M. Smullyan (1968) è il seguente: a) costruire l'albero generando i rami nell'ordine da sinistra a destra, ricominciando di nuovo da sinistra dopo aver trattato il ramo in quel momento più a destra; b) per ogni ramo applicare la regola appropriata alla formula più in alto, cancellandola dal ramo dopo averla trattata se non è una γ−formula. Se è una γ−formula, usare il primo termine t non contenente variabili (in un qualche ordine dei termini prefissato) tale che γ (t) non occorre nel ramo, eliminare l'occorrenza in questione e aggiungere un'occorrenza di γ alla fine del ramo. L'ordine di Smullyan va però incontro alla difficoltà che la γ−regola ci permette di usare un termine qualsiasi t non contenente variabili, e non ci dà alcuna guida per una scelta ''intelligente'' di t. Una buona soluzione consiste nel passare da γ a γ (a) dove a è una nuova pseudovariabile, e successivamente vedere se sostituendo a con qualche termine già occorrente nel ramo si ottiene un ramo chiuso. Ciò è illustrato dal seguente albero che mostra che ¬A(n, m) è una conseguenza di ∀x(A(x, m)→A(m, x)) e ¬A(m, n):

Qui il segno √ indica che la formula è eliminata dal ramo. Sostituendo a con n entrambi i rami dell'albero diventano chiusi.

Sebbene il metodo dei tableaux non abbia ancora prodotto linguaggi di programmazione ad alto livello di pratico impiego come il PROLOG, tuttavia è in corso un intenso lavoro di ricerca in tale direzione.

La sintesi logica dei programmi. − La programmazione logica e il PROLOG hanno reso popolare l'equazione: computare=dimostrare. Un ulteriore sviluppo di questa idea è di usare le dimostrazioni per estrarre da esse in modo meccanico dei programmi di computo. Non si può sperare, però, di ottenere questo da dimostrazioni qualsiasi, ma solo da una classe ristretta di dimostrazioni, le cosiddette dimostrazioni costruttive.

Ciò che v'è di caratteristico in una dimostrazione costruttiva può essere descritto nei termini seguenti. Supponiamo di avere una dimostrazione dell'esistenza di un oggetto avente una certa proprietà. Se si introducono opportune restrizioni sulla forma delle inferenze usate nella dimostrazione, allora la dimostrazione può permettere di scoprire un particolare oggetto avente quella proprietà. Una dimostrazione costruttiva ha tale caratteristica: una dimostrazione costruttiva di ∃xA(x) fornisce sempre un termine t tale che vale A(t).

Se la dimostrazione di esistenza viene data in modo formale, cioè in un modo che la rende adatta a essere manipolata meccanicamente, allora si può sperare di meccanizzare il passaggio dalla dimostrazione di ∃xA(x) al termine t tale che A(t). Le ricerche svolte nella branca della l. matematica nota col nome di teoria della dimostrazione hanno mostrato che tale meccanizzazione può essere ottenuta in molti modi. Per es. il procedimento di normalizzazione introdotto da Prawitz (1965) assolve in linea di principio − sebbene non efficientemente − a tale scopo. Più in generale, se si ha una dimostrazione costruttiva di ∀x∃yA(x, y), i procedimenti della teoria della dimostrazione possono servire per computare una funzione f tale che ∀xA(x, f(x)). Dunque una dimostrazione costruttiva di ∀x∃yA(x, y) ha il ruolo di un programma che computa una funzione f che soddisfa la ''specifica'' A.

Come si è già accennato i procedimenti standard della teoria della dimostrazione, come la normalizzazione di Prawitz, non sono però adeguati per estrarre programmi dalle dimostrazioni in modo efficiente, e quindi praticamente fattibile. Tuttavia le ricerche avviate da A.C. Goad (1980) hanno condotto all'introduzione di metodi che consentono di ovviare a questa difficoltà.

Bibl.: M.L. Minsky, Computation: finite and infinite machines, Englewood Cliffs 1967; R.M. Smullyan, First-order logic, Berlino 1968; C.L. Chang, R.C.T. Lee, Symbolic logic and mechanical theorem proving, New York 1973; W.S. Brainerd, L.H. Landweber, Theory of computation, ivi 1974; M. Machtey, P. Young, An introduction to the general theory of algorithms, ivi 1978; D.W. Loveland, Automated theorem proving: a logical basis, ivi 1978; J.A. Robinson, Logic: form and function, Edinburgo 1979; R.A. Kowalski, Logic for problem solving, New York 1979; P. Henderson, Functional programming, Englewood Cliffs 1980; A.C. Goad, Computational uses of the manipulation of formal proofs, Stanford 1980; W. Bibel, Automated theorem proving, Vieweg 1982; M.C. Fitting, Proof methods for modal and intuitionistic logic, Dordrecht 1983; A. Bundy, The computer modelling of mathematical reasoning, New York 1983 (trad. it., Padova 1986); G.J. Tourlakis, Computability, Reston 1984; H.P. Barendregt, The lambda calculus, its syntax and semantics, Amsterdam 1984; H. Glaser, C. Hankin, D. Till, Principles of functional programming, Londra 1984; C.J. Hogger, Introduction to logic programming, ivi 1984; J.W. Lloyd, Foundations of logic programming, Berlino 1984 (trad. it., Padova 1986); J.R. Hindley, J.P. Seldin, Introduction to combinators and λ-calculus Cambridge 1986; J.H. Gallier, Logic for computer science, New York 1986; I. Bratko, PROLOG: programming for artificial intelligence, Reading (Mass.) 1986 (trad. it., Milano 1988); L. Sterling, E. Shapiro, The art of PROLOG, Cambridge (Mass.) 1986; G.E. Revesz, Lambda-calculus, combinators and functional programming, Cambridge 1988.