Sintesi Tecnica: Azioni che Producono Obblighi nel Calcolo delle Situazioni

Definizione del Problema

Il documento affronta il problema del frame (frame problem) nel contesto delle azioni che producono obblighi nel Calcolo delle Situazioni. Mentre il lavoro seminale di Raymond Reiter ha fornito una soluzione al problema del frame per le azioni ordinarie (tramite assiomi di stato successore) e Scherl e Levesque lo hanno esteso alle azioni che producono conoscenza, un quadro completo per le azioni che producono obblighi rimaneva sottosviluppato.

Nello specifico, gli autori identificano una lacuna nel lavoro di Demolombe et al. [6], i quali hanno introdotto concetti deontici nel Calcolo delle Situazioni ma non hanno sviluppato un quadro completo per il ragionamento su queste azioni o per l'implementazione di specifiche. La sfida centrale consiste nel modellare formalmente azioni che creano obblighi per l'agente che le compie (ad esempio, sbloccare una porta crea l'obbligo di bloccarla in seguito) e nel determinare come tali obblighi persistano, cambino o terminino man mano che l'agente compie azioni successive, senza dover elencare esplicitamente tutti i fatti legali non influenzati.

Metodologia

Gli autori propongono una soluzione basata sulle Basic Action Theories di Reiter e sulla semantica dei mondi possibili di tipo Kripke per la logica deontica, evitando l'ordinamento di "idealità" delle situazioni utilizzato nelle formulazioni precedenti.

1. Quadro Formale

L'approccio utilizza una versione temporale del Calcolo delle Situazioni con sortamenti per azioni, situazioni, punti temporali e oggetti.

• Fluente Deontico ($O$): Viene introdotta una relazione binaria $O(s', s)$, che denota che la situazione $s'$ è deonticamente accessibile dalla situazione $s$.
• Operatore di Obbligo: Un obbligo $Oblg(\phi, s)$ è definito come un operatore di necessità sulla relazione di accessibilità: $(\forall s'). O(s', s) \supset \phi[s']$. Ciò significa che $\phi$ è obbligatorio in $s$ se è vero in tutte le situazioni deonticamente accessibili.
• Classificazione delle Azioni: Le azioni sono categorizzate in tre tipi riguardo al loro effetto sugli obblighi:
  1. Azioni che non producono obblighi: Azioni ordinarie che non creano né rilasciano obblighi.
  2. Azioni che rilasciano obblighi: Azioni che interrompono gli obblighi esistenti (ad esempio, notificare un responsabile dopo aver bloccato una porta).
  3. Azioni che producono obblighi: Azioni che creano nuovi obblighi (ad esempio, sbloccare una porta crea l'obbligo di bloccarla).

2. Assiomi di Stato Successore per $O$

Il nucleo del contributo tecnico è la derivazione di un Assioma di Stato Successore (SSA) per il fluente deontico $O$. Questo assioma caratterizza come l'insieme delle situazioni deonticamente accessibili cambi dopo che un'azione $a$ viene eseguita nella situazione $s$:

• Per le azioni che non producono obblighi: Le situazioni accessibili nello stato successivo sono semplicemente le immagini delle situazioni accessibili nello stato corrente sotto l'azione $a$.
• Per le azioni che rilasciano obblighi: L'assioma filtra le situazioni accessibili in cui la condizione per l'obbligo (il fluente associato) è stata soddisfatta, rimuovendo efficacemente quei percorsi dallo spazio deontico.
• Per le azioni che producono obblighi: L'assioma restringe le situazioni accessibili a quelle in cui il nuovo obbligo creato è soddisfatto. Nello specifico, se l'azione $a$ crea un obbligo per il fluente $F$, le nuove situazioni accessibili sono quelle in cui $F$ è vero.

3. Regressione per gli Obblighi

Il documento estende l'operatore di regressione di Reiter per gestire le formule di obbligo. Ciò consente di ridurre il ragionamento sulla verità delle affermazioni di obbligo in situazioni future al ragionamento sulla situazione iniziale ($S_0$).

• Gli autori definiscono un operatore di regressione $R$ che gestisce il predicato $Oblg$.
• L'operatore trasforma ricorsivamente le formule che coinvolgono obblighi in situazioni successive in formule equivalenti nella situazione iniziale, utilizzando gli assiomi di stato successore sia per i fluenti ordinari che per il fluente deontico $O$.
• Viene dimostrato un Teorema di Regressione, il quale afferma che una frase $W$ è implicata da una teoria di base se e solo se la sua forma completamente regredita è implicata dagli assiomi della situazione iniziale aumentati dagli assiomi di nome unico e dalle proprietà specifiche della relazione $O$ (come serialità e riflessività).

Contributi Chiave

1. Semplificazione della Formalizzazione: Il documento semplifica la caratterizzazione della relazione di accessibilità eliminando la nozione di "idealità" delle situazioni, allineandosi così più strettamente alla semantica standard dei mondi possibili per la logica deontica (specificamente la Standard Deontic Logic).
2. Teoria dell'Azione Completa: Fornisce un insieme completo di assiomi (fondamentali, di precondizione, di stato successore e di nome unico) che estendono il framework di Reiter per includere le azioni che producono obblighi.
3. Dimostrazioni di Correttezza: Gli autori dimostrano che la loro formalizzazione produce proprietà intuitive:
   • Creazione: L'esecuzione di un'azione che produce un obbligo crea l'obbligo corrispondente nella situazione successiva.
   • Persistenza: Gli obblighi persistono nelle situazioni successive a meno che non vengano esplicitamente interrotti.
   • Terminazione: Gli obblighi vengono rimossi quando il fluente associato diventa vero (o quando viene eseguita una specifica azione di rilascio).
4. Estensione della Regressione: Il documento estende il teorema di regressione al dominio degli obblighi, consentendo il ragionamento automatizzato su contratti legali e smart contract all'interno del Calcolo delle Situazioni.

Risultati

Il documento dimostra che la formalizzazione proposta modella correttamente la dinamica degli obblighi. Utilizzando un esempio ricorrente di uno scenario di apertura porta (sbloccare, bloccare e notificare un responsabile), gli autori mostrano:

• Come la relazione di accessibilità $O$ evolva man mano che le azioni vengono eseguite.
• Come l'operatore di regressione riesca a ridurre query di obbligo complesse in situazioni future a condizioni verificabili nella situazione iniziale.
• Il sistema supporta la verifica di proprietà quali "se una frase è obbligatoria in una situazione, essa rimane tale nelle situazioni successive a meno che l'obbligo non venga esplicitamente interrotto".

Significato e Rivendicazioni

Gli autori sostengono che questo lavoro fornisce una base semantica rigida per la specifica e il ragionamento automatizzato di documenti legali e smart legal contract. Formalizzando gli obblighi direttamente nel Calcolo delle Situazioni, l'approccio:

• Evita la necessità di passaggi di compilazione extra richiesti da altri approcci (ad esempio, metodi basati su vincoli).
• Sfrutta strumenti esistenti come GOLOG (un linguaggio di programmazione basato sul Calcolo delle Situazioni) per definire azioni complesse e verificare accordi legali.
• Offre una soluzione al problema del frame specificamente progettata per la logica deontica, garantendo che gli agenti di ragionamento legale possano tracciare i cambiamenti di diritti e doveri senza alterare accidentalmente fatti legali non correlati.

Il documento si pone come un passo necessario verso l'implementazione di smart legal contract che possano essere formalmente verificati per coerenza ed esecuzione affidabile in ambienti dinamici e distribuiti. Il lavoro futuro è identificato nell'estensione di questo framework per gestire le violazioni delle norme e gli obblighi contrari al dovere (contrary-to-duty obligations).