Modeling Deontic Modal Logic in ASP

Imagine que você é o árbitro de um jogo gigante e invisível de "E se?" acontecendo dentro do cérebro de um computador. No mundo da lógica, existem duas formas principais de falar sobre regras. A primeira é como uma equação matemática rigorosa: "Se A é verdadeiro, então B deve ser verdadeiro". Isso é a lógica clássica, e é ótima para fatos. Mas a segunda forma é muito mais humana: "Você deveria fazer B", ou "É proibido fazer A", ou "Você tem permissão para fazer B". Isso é chamado de lógica deôntica (da palavra grega para "dever"). É a lógica das regras, leis e obrigações morais. A parte complicada é que a vida real é bagunçada. Às vezes você tem a obrigação de fazer algo, mas não consegue. Às vezes você é proibido de fazer algo, mas faz mesmo assim. Por décadas, cientistas da computação e filósofos lutaram para ensinar computadores a lidar com esses "deveria" e "proibidos" sem ficarem confusos ou travarem em contradições lógicas conhecidas como "paradoxos".

Este artigo, intitulado "Modeling Deontic Modal Logic in ASP", aborda exatamente esse problema. Os autores, uma equipe de pesquisadores dos EUA e da Espanha, propõem uma nova maneira inteligente de ensinar computadores a entender regras e obrigações. Eles usam uma linguagem de programação chamada Programação de Conjuntos de Respostas (ASP), que já é famosa por sua capacidade de lidar com cenários de "e se?" e informações incompletas. O artigo argumenta que, ao tratar as regras não como comandos rígidos que forçam fatos a acontecerem, mas como restrições globais (como o apito de um árbitro que toca se uma regra for quebrada), os computadores podem finalmente resolver enigmas antigos, de décadas atrás, que deixaram os lógicos perplexos. Eles mostram que este método resolve elegantemente armadilhas lógicas famosas, como o paradoxo "Contrário ao Dever" (Contrary-to-Duty), onde uma regra parece se contradizer quando uma pessoa falha em seguir uma regra anterior.

A Magia do "Deveria" e do "Deve"

Para entender o que os autores fizeram, primeiro precisamos conhecer os dois personagens principais de sua história: Obrigação e Permissão. Na vida cotidiana, sabemos a diferença entre "É necessário que o sol nasça" (um fato da natureza) e "Você deve devolver seu livro da biblioteca" (uma regra que você pode quebrar). No mundo da lógica, o primeiro é chamado de alético (sobre verdade e necessidade) e o segundo é deôntico (sobre dever e normas).

Os autores notaram que os computadores já possuem duas ferramentas especiais para lidar com esses diferentes tipos de pensamento, mas elas estavam sendo usadas da maneira errada.

1. Negação Forte: Isso é como um "Não" absoluto. Se um computador diz "Não está chovendo" (negação forte), significa que ele tem provas de que definitivamente não está chovendo. É um fato.
2. Negação por Falha (Negação como Falha): Isso é como um "Talvez não". Se um computador diz "Não está chovendo" (negação por falha), significa apenas que ele não encontrou evidências de que está chovendo. É um palpite baseado na falta de informação.

A grande ideia do artigo é mapear essas duas ferramentas de computador diretamente para os dois tipos de lógica. Eles sugerem que, quando falamos de "É necessário que P" (um fato), usamos a Negação Forte. Mas quando falamos de "Não é necessário que P" (significando que P pode ser falso, ou simplesmente não sabemos), usamos a Negação por Falha. Essa mudança simples permite que o computador distinga entre um fato duro e uma regra que pode ser quebrada.

A Abordagem do "Árbitro"

A parte mais criativa do artigo é como eles lidam com as obrigações. Em muitos sistemas antigos, uma obrigação como "Você deve devolver o carro" era tratada como um comando que força o computador a fazer o carro ser devolvido. Mas e se o carro for roubado? O computador travaria porque não consegue forçar a devolução do carro.

Os autores propõem uma abordagem diferente: tratar as obrigações como Restrições Globais (ou "Denegações"). Imagine um árbitro em um jogo de futebol. O árbitro não força os jogadores a marcarem gols; o árbitro apenas apita se ocorrer uma falta. No sistema dos autores, uma obrigação não é um comando para fazer algo ser verdadeiro; é uma regra que diz: "Se você estiver em um mundo onde esta regra é quebrada, esse mundo é inválido".

Por exemplo, se a regra é "Você deve usar o cinto de segurança", o computador não força você a usá-lo. Em vez disso, ele estabelece uma restrição: "Qualquer mundo onde você esteja dirigindo sem o cinto de segurança é descartado". Se você estiver dirigindo e não tiver o cinto, o computador simplesmente diz: "Esse cenário é impossível sob estas regras", e procura por um cenário diferente onde você tenha o cinto de segurança. Mas, crucialmente, se você tiver um motivo válido para não usar o cinto (como uma emergência médica), o computador pode "preceder" a regra. Ele descarta a restrição para essa situação específica, permitindo que o cenário exista sem causar um erro no sistema.

Resolvendo o Enigma de "Chisholm"

O artigo brilha intensamente quando resolve o Paradoxo do Contrário ao Dever (tambamente conhecido como o Paradoxo de Chisholm), que é um famoso problema lógico que segue este fluxo:

1. Você deve ir à festa.
2. Se você for, deve contar para sua mãe.
3. Se você não for, não deve contar para sua mãe.
4. Você não vai.

Em sistemas lógicos antigos, isso cria uma bagunça. O computador tenta descobrir se você deve ou não contar para sua mãe e acaba com uma contradição: você deve e não deve contar para ela ao mesmo tempo. É como um robô tendo uma dor de cabeça.

Os autores mostram que o método do "Árbitro" resolve isso instantaneamente. Eles configuram as regras como restrições:

• Restrição 1: Se você não for, você não pode contar para sua mãe.
• Restrição 2: Se você for, você deve contar para sua mãe.

Quando o computador vê que você não foi (Fato 4), ele verifica as restrições. Ele vê que a Restrição 2 (a regra "Se você for") não se aplica porque a condição não foi atendida. Ele então olha para a Restrição 1. Como você não foi, a regra diz "Não conte". O computador encontra facilmente um mundo válido onde você não foi e não contou para sua mãe. Sem contradição, sem dor de cabeça. O "paradoxo" desaparece porque as regras são tratadas como restrições flexíveis que só se aplicam quando suas condições são atendidas, em vez de comandos rígidos que lutam entre si.

Por Que Isso Importa

Os autores não apenas resolvem um enigma; eles mostram que este método funciona para toda uma família de problemas lógicos, incluindo o "paradoxo de Forrester" e o "dilema de Sartre". Eles demonstram que, ao usar a Programação de Conjuntos de Respostas com sua capacidade integrada de lidar com cenários de "e se?" e "exceções", podemos modelar sistemas éticos e legais complexos de forma muito mais natural do que antes.

Eles também mostram como isso lida com "obrigações secundárias". Imagine que você pegou o carro de um amigo emprestado. Você tem uma regra principal: "Devolver o carro". Mas existem regras secundárias: "Devolver antes do meio-dia" e "Devolver com a bateria cheia". Se você bater o carro (uma violação da regra principal), as regras secundárias podem mudar ou desaparecer. Os autores mostram como seu sistema pode "preceder" essas regras automaticamente. Se o carro estiver destruído, a restrição "Devolver antes do meio-dia" é descartada porque a condição (ter um carro para devolver) deixou de existir. O computador não fica confuso; ele apenas atualiza a lista de mundos válidos.

A Conclusão

Este artigo não afirma ter resolvido todos os problemas da ética ou do direito. Em vez disso, oferece um conjunto de ferramentas limpo e elegante para construir sistemas que entendam regras. Ele prova que, ao tratar os "deveria" como restrições sobre mundos possíveis em vez de comandos para mudar a realidade, podemos construir computadores que raciocinam sobre regras da mesma forma que os humanos: de forma flexível, com exceções e sem ficar presos em loops lógicos. Os autores sugerem que esta abordagem é mais simples e direta do que métodos anteriores, que muitas vezes exigiam matemática complexa ou "sanções" (punições) para fazer a lógica funcionar. Ao usar as ferramentas já disponíveis na Programação de Conjuntos de Respostas, eles mostraram que o caminho para entender regras humanas pode ser mais curto e direto do que pensávamos.