Resumo Técnico: Ações Produtoras de Obrigações no Cálculo de Situações

Definição do Problema

O artigo aborda o problema do quadro (frame problem) no contexto de ações produtoras de obrigações no Cálculo de Situações. Embora o trabalho seminal de Raymond Reiter tenha fornecido uma solução para o problema do quadro para ações comuns (via axiomas de estado sucessor) e Scherl e Levesque tenham estendido isso para ações produtoras de conhecimento, um arcabouço completo para ações produtoras de obrigações permanecia subdesenvolvido.

Especificamente, os autores identificam uma lacuna no trabalho de Demolombe et al. [6], que introduziram conceitos deonticos no Cálculo de Situações, mas não desenvolveram um arcabouço completo para o raciocínio sobre essas ações ou para a implementação de especificações. O desafio central é modelar formalmente ações que criam obrigações para o agente que as realiza (por exemplo, destrancar uma porta cria a obrigação de trancá-la mais tarde) e determinar como essas obrigações persistem, mudam ou terminam conforme o agente realiza ações subsequentes, sem listar explicitamente todos os fatos legais não afetados.

Metodologia

Os autores propõem uma solução fundamentada nas Teorias de Ação Básica de Reiter e na semântica de mundos possíveis do tipo Kripke para a lógica deontica, evitando a ordenação de "idealidade" de situações utilizada em formulações anteriores.

1. Arcabouço Formal

A abordagem utiliza uma versão temporal do Cálculo de Situações com tipos (sorts) para ações, situações, pontos temporais e objetos.

• Fluente Deontico ($O$): Uma relação binária $O(s', s)$ é introduzida, denotando que a situação $s'$ é deonticamente acessível a partir da situação $s$.
• Operador de Obrigação: Uma obrigação $Oblg(\phi, s)$ é definida como um operador de necessidade sobre a relação de acessibilidade: $(\forall s'). O(s', s) \supset \phi[s']$. Isso significa que $\phi$ é obrigatório em $s$ se for verdadeiro em todas as situações deonticamente acessíveis.
• Classificação de Ações: As ações são categorizadas em três tipos em relação ao seu efeito sobre as obrigações:
  1. Ações não produtoras de obrigações: Ações comuns que não criam nem liberam obrigações.
  2. Ações de liberação de obrigações: Ações que interrompem obrigações existentes (ex: notificar um gerente após trancar uma porta).
  3. Ações produtoras de obrigações: Ações que criam novas obrigações (ex: destrancar uma porta cria a obrigação de trancá-la).

2. Axiomas de Estado Sucessor para $O$

A principal contribuição técnica é a derivação de um Axioma de Estado Sucessor (SSA) para o fluente deontico $O$. Este axioma caracteriza como o conjunto de situações deonticamente acessíveis muda após uma ação $a$ ser realizada na situação $s$:

• Para ações não produtoras de obrigações: As situações acessíveis no estado sucessor são simplesmente as imagens das situações acessíveis no estado atual sob a ação $a$.
• Para ações de liberação de obrigações: O axioma filtra as situações acessíveis onde a condição para a obrigação (o fluente associado) foi satisfeita, removendo efetivamente esses caminhos do espaço deontico.
• Para ações produtoras de obrigações: O axioma restringe as situações acessíveis àquelas onde a nova obrigação criada é satisfeita. Especificamente, se a ação $a$ cria uma obrigação para o fluente $F$, as novas situações acessíveis são aquelas onde $F$ é verdadeiro.

3. Regressão para Obrigações

O artigo estende o operador de regressão de Reiter para lidar com fórmulas de obrigação. Isso permite que o raciocínio sobre a verdade de sentenças de obrigação em situações futuras seja reduzido ao raciocínio sobre a situação inicial ($S_0$).

• Os autores definem um operador de regressão $R$ que lida com o predicado $Oblg$.
• O operador transforma recursivamente fórmulas envolvendo obrigações em situações sucessoras em fórmulas equivalentes na situação inicial, utilizando os axiomas de estado sucessor tanto para fluentes comuns quanto para o fluente deontico $O$.
• Um Teorema de Regressão é provado, afirmando que uma sentença $W$ é implicada por uma teoria de ação básica se, e somente se, sua forma totalmente regredida for implicada pelos axiomas da situação inicial aumentados com axiomas de nomes únicos e propriedades específicas da relação $O$ (como serialidade e reflexividade).

Principais Contribuições

1. Formalização Simplificada: O artigo simplifica a caracterização da relação de acessibilidade ao eliminar a noção de "idealidade" das situações, alinhando-se mais de perto com a semântica Kripke padrão para a lógica deontica (especificamente a Lógica Deontica Padrão).
2. Teoria de Ação Completa: Fornece um conjunto completo de axiomas (fundacionais, de precondição, de estado sucessor e de nomes únicos) estendendo o arcabouço de Reiter para incluir ações produtoras de obrigações.
3. Provas de Correção: Os autores provam que sua formalização produz propriedades intuitivas:
   • Criação: Realizar uma ação produtora de obrigação cria a obrigação correspondente na situação sucessora.
   • Persistência: As obrigações persistem em situações subsequentes, a menos que sejam explicitamente interrompidas.
   • Terminação: As obrigações são removidas quando o fluente associado torna-se verdadeiro (ou quando uma ação de liberação específica é realizada).
4. Extensão da Regressão: O artigo estende o teorema de regressão para o domínio das obrigações, permitindo o raciocínio automatizado sobre contratos legais e contratos inteligentes dentro do Cálculo de Situações.

Resultados

O artigo demonstra que a formalização proposta modela corretamente a dinâmica das obrigações. Usando um exemplo recorrente de um cenário de abertura de porta (destrancar, trancar e notificar um gerente), os autores mostram:

• Como a relação de acessibilidade $O$ evolui conforme as ações são realizadas.
• Como o operador de regressão reduz com sucesso consultas complexas de obrigação em situações futuras para condições verificáveis na situação inicial.
• O sistema suporta a verificação de propriedades como "se uma sentença é obrigatória em uma situação, ela permanece assim em situações subsequentes, a menos que a obrigação seja explicitamente interrompida".

Significância e Alegações

Os autores alegam que este trabalho fornece uma base semântica rígida para a especificação e o raciocínio automatizado de documentos legais e contratos jurídicos inteligentes (smart legal contracts). Ao formalizar as obrigações diretamente dentro do Cálculo de Situações, a abordagem:

• Evita a necessidade de etapas extras de compilação exigidas por outras abordagens (ex: métodos baseados em restrições).
• Aproveita ferramentas existentes como o GOLOG (uma linguagem de programação baseada no Cálculo de Situações) para definir ações complexas e verificar acordos legais.
• Oferece uma solução para o problema do quadro especificamente adaptada para a lógica deontica, garantindo que agentes de raciocínio jurídico possam rastrear mudanças em direitos e deveres sem alterar acidentalmente fatos legais não relacionados.

O artigo posiciona-se como um passo necessário para a implementação de contratos jurídicos inteligentes que podem ser formalmente verificados para consistência e execução confiável em ambientes dinâmicos e distribuídos. O trabalho futuro é identificado como a extensão deste arcabouço para lidar com violações de normas e obrigações de dever contrário (contrary-to-duty obligations).