Modeling Deontic Modal Logic in ASP

Immagina di essere il arbitro di un gigantesco e invisibile gioco di "E se...?" che si svolge all'interno del cervello di un computer. Nel mondo della logica, esistono due modi principali per parlare di regole. Il primo è come una rigida equazione matematica: "Se A è vero, allora B deve essere vero". Questa è la logica classica, ed è ottima per i fatti. Ma il secondo modo è molto più umano: "Dovresti fare B", oppure "È vietato fare A", o ancora "Ti è permesso fare B". Questa è la logica deontica (dal termine greco per "dovere"). È la logica delle regole, delle leggi e degli obblighi morali. La parte complicata è che la vita reale è disordinata. A volte hai l'obbligo di fare qualcosa, ma non puoi farlo. A volte ti è vietato fare qualcosa, ma lo fai comunque. Per decenni, scienziati informatici e filosofi hanno lottato per insegnare ai computer come gestire questi "dovresti" e "vietati" senza confondersi o andare in crash a causa di contraddizioni logiche note come "paradossi".

Questo articolo, intitolato "Modeling Deontic Modal Logic in ASP", affronta esattamente questo problema. Gli autori, un team di ricercatori provenienti dagli Stati Uniti e dalla Spagna, propongono un nuovo e intelligente modo per insegnare ai computer come comprendere le regole. Utilizzano un linguaggio di programmazione chiamato Answer Set Programming (ASP), che è già famoso per la sua capacità di gestire scenari "e se...?" e informazioni incomplete. L'articolo sostiene che trattando le regole non come comandi rigidi che costringono i fatti ad accadere, ma come vincoli globali (come il fischietto di un arbitro che suona se una regola viene infranta), i computer possano finalmente risolvere vecchi enigmi che hanno messo in difficoltà i logici per decenni. Dimostrano che questo metodo risolve elegantemente famosi trabocchetti logici, come il paradosso "Contrario al Dovere" (Contrary-to-Duty), in cui una regola sembra contraddire se stessa quando una persona non segue una regola precedente.

La magia del "Doveri" e del "Deve"

Per capire cosa hanno fatto gli autori, dobbiamo prima incontrare i due personaggi principali della loro storia: l'Obbligo e il Permesso. Nella vita di tutti i giorni, conosciamo la differenza tra "È necessario che il sole sorga" (un fatto della natura) e "Dovresti restituire il libro della biblioteca" (una regola che potresti infrangere). Nel mondo della logica, il primo è chiamato aletico (riguardante la verità e la necessità), e il secondo è deontico (riguardante il dovere e le norme).

Gli autori hanno notato che i computer possiedono già due strumenti speciali per gestire questi diversi tipi di pensiero, ma venivano usati nel modo sbagliato.

1. Negazione Forte: Questa è come un duro "No". Se un computer dice "Non sta piovendo" (negazione forte), significa che ha la prova che non sta sicuramente piovendo. È un fatto.
2. Negazione di Default (Negazione per Fallimento): Questa è come un "Forse no". Se un computer dice "Non sta piovendo" (negazione di default), significa solo che non ha trovato prove che stia piovendo. È un'ipotesi basata su informazioni mancanti.

La grande idea dell'articolo è quella di mappare questi due strumenti informatici direttamente sui due tipi di logica. Suggeriscono che quando parliamo di "È necessario che P" (un fatto), usiamo la Negazione Forte. Ma quando parliamo di "Non è necessario che P" (intendendo che P potrebbe essere falso, o semplicemente non lo sappiamo), usiamo la Negazione di Default. Questo semplice scambio permette al computer di distinguere tra un fatto certo e una regola che può essere infranta.

L'approccio dell'"Arbitro"

La parte più creativa dell'articolo riguarda il modo in cui gestiscono gli obblighi. In molti sistemi datati, un obbligo come "Devi restituire l'auto" veniva trattato come un comando che forza il computer a far sì che l'auto venga restituita. Ma cosa succede se l'auto viene rubata? Il computer andrebbe in crash perché non può forzare la restituzione dell'auto.

Gli autori propongono un approccio diverso: trattare gli obblighi come Vincoli Globali (o "Negazioni"). Immaginate un arbitro in una partita di calcio. L'arbitro non forza i giocatori a segnare; l'arbitro si limita a fischiare se avviene un fallo. Nel sistema degli autori, un obbligo non è un comando per rendere vero qualcosa; è una regola che dice: "Se ti trovi in un mondo in cui questa regola è infranta, quel mondo è invalido".

Per esempio, se la regola è "Devi indossare la cintura di sicurezza", il computer non ti forza a indossarla. Invece, imposta un vincolo: "Qualsiasi mondo in cui stai guidando senza la cintura di sicurezza viene scartato". Se stai guidando e non indossi la cintura, il computer semplicemente dice: "Questo scenario è impossibile secondo queste regole", e cerca un altro scenario in cui la cintura la indossi. Ma, cosa fondamentale, se hai un motivo valido per non indossarla (come un'emergenza medica), il computer può "prevenire" la regola. Esso scarta il vincolo per quella specifica situazione, permettendo allo scenario di esistere senza andare in crash.

Risolvere l'enigma di "Chisholm"

L'articolo brilla soprattutto quando risolve il Paradosso del Contrario al Dovere (noto anche come Paradosso di Chisholm). Questo è un celebre mal di testa logico che procede così:

1. Dovresti andare alla festa.
2. Se vai, devi dirlo a tua madre.
3. Se non vai, non dovresti dirlo a tua madre.
4. Tu non vai.

Nei vecchi sistemi logici, questo crea un caos. Il computer cerca di capire se dovresti dirlo a tua madre o meno, e finisce con una contraddizione: dovresti dirlo e non dovresti dirlo contemporaneamente. È come un robot che ha il mal di testa.

Gli autori dimostrano che il loro metodo dell' "Arbitro" risolve questo problema istantaneamente. Impostano le regole come vincoli:

• Vincolo 1: Se non vai, non puoi dirlo a tua madre.
• Vincolo 2: Se vai, devi dirlo a tua madre.

Quando il computer vede che tu non sei andato (Fatto 4), controlla i vincoli. Nota che il Vincolo 2 (la regola "Se vai") non si applica perché la condizione non è stata soddisfatta. Successivamente, esamina il Vincolo 1. Poiché non sei andato, la regola dice "Non dirlo". Il computer trova facilmente un mondo valido in cui non sei andato e non l'hai detto a tua madre. Nessuna contraddizione, nessun mal di testa. Il "paradosso" svanisce perché le regole sono trattate come vincoli flessibili che si applicano solo quando le loro condizioni sono soddisfatte, piuttosto che come comandi rigidi che si scontrano tra loro.

Perché questo è importante

Gli autori non si limitano a risolvere un singolo enigma; dimostrano che questo metodo funziona per un'intera famiglia di problemi logici, inclusi il "paradosso di Forrester" e il "dilemma di Sartre". Dimostrano che utilizzando l'Answer Set Programming, con la sua capacità integrata di gestire scenari "e se...?" ed "eccezioni", possiamo modellare sistemi etici e legali complessi in modo molto più naturale rispetto al passato.

Mostrano anche come questo gestisca gli "obblighi secondari". Immaginate di prendere in prestito l'auto di un amico. Avete una regola principale: "Restituisci l'auto". Ma ci sono regole secondarie: "Restituiscila prima di mezzogiorno" e "Restituiscila con la batteria carica". Se fate incidenti con l'auto (una violazione della regola principale), le regole secondarie potrebbero cambiare o scomparire. Gli autori mostrano come il loro sistema possa "prevenire" queste regole automaticamente. Se l'auto è distrutta, il vincolo "Restituisci prima di mezzogiorno" viene scartato perché la condizione (avere un'auto da restituire) è venuta meno. Il computer non si confonde; aggiorna semplicemente l'elenco dei mondi validi.

In sintesi

Questo articolo non pretende di aver risolto ogni problema di etica o di legge. Al contrario, offre un toolkit pulito ed elegante per costruire sistemi che comprendano le regole. Dimostra che trattando i "doveri" come vincoli sui mondi possibili anziché come comandi per cambiare la realtà, possiamo costruire computer che ragionano sulle regole come fanno gli esseri umani: in modo flessibile, con eccezioni e senza incastrarsi in loop logici. Gli autori suggeriscono che questo approccio sia più semplice e diretto rispetto ai metodi precedenti, che spesso richiedevano nuove e complesse strutture matematiche o "sanzioni" (punizioni) per far funzionare la logica. Utilizzando gli strumenti già disponibili nell'Answer Set Programming, hanno dimostrato che la strada per comprendere le regole umane potrebbe essere più breve e lineare di quanto pensassimo.