Lógica de Primeira Ordem II
Tal como para a Lógica Proposicional, é possível automatizar alguns aspetos relacionados com a Lógica de Primeira Ordem. Em relação ao sistema dedutivo, vamos voltar a olhar para a resolução. Além disso, olhamos agora para a Lógica de Primeira Ordem como forma de representar conhecimento sobre um dado contexto - um mundo.
Representação do Conhecimento
Aviso
Se estiverem apenas a estudar para a avaliação das práticas, as secções dos agentes cognitivos e das hipóteses subjacentes não são particularmente relevantes. A secção Representar Conhecimento em Lógica volta a ser relevante para esse propósito.
Tem como objetivo principal fornecer a um computador declarações sobre um domínio, com vista a permitir que o próprio computador realize operações inteligentes sobre esse mesmo domínio. Ligada à área da Inteligência Artificial.
Agentes cognitivos
A inteligência artificial constrói programas que agem tendo por base uma representação do conhecimento, os agentes cognitivos. São sensores que permitem que o computador se aperceba e possa agir em relação ao mundo que o rodeia; os procedimentos têm apenas por base aquilo que o computador sabe sobre o mundo.
Os agentes cognitivos têm como componentes principais a base de conhecimento, que contém uma representação do mundo, e o motor de inferência, conjunto de procedimentos independentes do conhecimento representado que manipulam a base do conhecimento.
Existem duas hipóteses (dizem-se hipóteses porque ainda não foi provado que são falsas) importantes em relação a este tipo de sistemas - a hipótese do sistema de símbolos físicos e a hipótese de representação do conhecimento.
A primeira consiste em ter um sistema de símbolos físicos compostos por um conjunto de entidades, os tais símbolos, que correspondem a "padrões físicos", que podem ser agrupados em estruturas, e por um conjunto de procedimentos que operam sobre eles. Haverá uma máquina a produzir sucessões de estruturas de símbolos, que contém memória para guardar informação sobre eles, entre outras propriedades.
- Qualquer sistema que apresente comportamento inteligente pode ser visto como um sistema de símbolos físicos - aplica-se a humanos por exemplo, onde os símbolos físicos aplicam-se na nossa memória. O nosso cérebro reage conforme identifica (ou não) um dado padrão, e tem capacidade de o memorizar.
- Qualquer sistema de símbolos físicos de tamanho adequado (não qualquer programa) pode ser organizado de modo a exibir comportamento inteligente.
Esta hipótese afirma, portanto, que é possível escrever um programa, um sistema de símbolos físicos, que exibe comportamento inteligente (aqui, inteligente no sentido de entidades inteligentes que surjam no mundo que nos rodeia, não no sentido de uma calculadora).
A segunda, a hipótese de representação do conhecimento, complementa a hipótese anterior. Diz-nos que qualquer processo mecânico que exibe comportamento inteligente é composto por estruturas, atribuídas por um observador externo, a uma representação proposicional do conhecimento usado por esse mesmo processo. Desempenham um papel formal, causal e essencial no comportamento que esse conhecimento manifesta. As tais estruturas proposicionais abrangem qualquer estrutura de dados, dos grafos às matrizes, estruturas essas armazenadas na base de conhecimento. Afirma, ainda, que é o conhecimento representado, independentemente de como o representamos, que gera o comportamento do sistema.
Representar Conhecimento em Lógica
Modelar o que pretendemos representar
O primeiro passo a tomar é inventar um modelo daquilo que pretendemos representar.
Consideramos um modelo como uma abstração do mundo, que apenas captura os seus aspetos relevantes para um certo problema ou tarefa. Neste modelo, devemos definir as entidades do mundo sobre as quais queremos falar, o universo do discurso, e as funções e relações que vamos utilizar. Estamos, assim, a definir o vocabulário utilizado pelas fbfs da representação escolhida. Depois de tomadas essas decisões, escrevemos as fbfs que relacionam constantes, funções e/ou relações: dizem-se axiomas próprios, proposições aceites sem prova em relação ao domínio atual.
O conjunto de todas as constantes, funções, relações e axiomas próprios é a ontologia do domínio.
Consideremos a seguinte definição de vocabulário, vocabulário esse a ser utilizado nos restantes exemplos desta secção:
Definição do Vocabulário
Vamos ter um conjunto de constantes, que, neste contexto, corresponderão a algumas personagens da série The Simpsons.
Vamos ainda ter o seguinte conjunto de relações, unárias e binárias:
Com o vocabulário apresentado acima, podemos escrever algumas fórmulas chãs:
Podemos ainda escrever algumas fbfs, aqui já com variáveis individuais:
Podemos até realizar provas utilizando estas representações! Na prova abaixo, vamos chegar à conclusão que é de , partindo de um conjunto de informações iniciais.
Forma Clausal
Obtida de forma semelhante à da Lógica Proposicional, contando com algumas diferenças.
Eliminação do símbolo
Funciona de igual forma à lógica proposicional.
Redução do domínio de
Igual à lógica proposicional, tendo ainda a adição das segundas leis de De Morgan.
A primeira afirma que "dizer que nem todo o tem uma certa propriedade é o mesmo que dizer que há pelo menos um que não a tem".
Por outro lado, a segunda afirma que "dizer que não há nenhum que tenha uma certa propriedade é o mesmo que dizer que todo o não tem a falta dessa propriedade".
Entra aqui um passo novo: a normalização de variáveis.
Normalização de variáveis
As ocorrências ligadas (dentro do domínio do quantificador) correspondem a variáveis mudas (irrelevantes para o valor da operação - por exemplo, em , é uma variável muda). A normalização de variáveis consiste em mudar o nome de algumas das variáveis, de modo a que o quantificador esteja associado a um único nome de variável - o objetivo é não haver quantificadores associados às mesmas variáveis dentro do domínio de um quantificador.
Pegando num exemplo mais concreto,
passa, através da normalização de variáveis, a:
Note-se que, caso os quantificadores interiores estivessem fora do domínio do quantificador , a normalização de variáveis não ocorreria!
Eliminação dos quantificadores existenciais
Fase separada em dois passos:
-
Eliminar quantificadores isolados - substituímos a fbf por , onde é uma nova constante - a constante de Skolem. A constante de Skolem é considerada a entidade que verifica a propriedade , apesar de nada sabermos em concreto sobre ela. Só pode ser aplicada a quantificadores isolados, fora do domínio de outros quantificadores.
-
Verificar dependências entre quantificadores existenciais e universais - se um quantificador existencial aparecer dentro do domínio de um quantificador universal, existe a possibilidade do valor da variável quantificada existencialmente depender do valor da variável quantificada universalmente. Caso dependa, substituímos a variável por um novo símbolo de função - função de Skolem, . Aqui, "a variável de dentro depende/é função da de fora; o (interior) depende/é função de (exterior)". A existência do está diretamente dependente de qual é o em questão, e é daí que vem a noção de função.
Exemplos
Podemos passar
para
Aqui, o valor de depende do de , pelo que para eliminar o quantificador existencial é necessário substituir a variável associada por um termo formado por um novo símbolo de função. é uma função de Skolem. Ao tentar substituir por uma constante de Skolem, obteríamos uma afirmação falsa (algo do género "Há um natural maior que todos os outros").
Temos então, portanto, que se nenhum quantificador universal aparecer "por fora" de um dado quantificador existencial, substituímos todas as ocorrências da variável a ele ligada pela constante de Skolem e removemos o quantificador; caso contrário, removemos também o quantificador, mas em vez de substituir a variável pela constante, substituímos pela função de Skolem.
Conversão para a forma Prenex normal
Todas as ocorrências de quantificadores universais são passadas para a esquerda. Vem de uma afirmação que fizemos mais atrás, onde dissemos que queremos sempre as representações o mais sucintas possível: se podemos condensar a nossa representação utilizando um único quantificador, fá-lo-emos.
Um exemplo seria, por exemplo, passar de
para
Eliminação da Quantificação Universal
Sendo que não há variáveis livres, e que todas elas estão quantificadas universalmente, a presença do quantificador acaba por ser irrelevante, visto que, lá está, as propriedades são universais. Podemos, agora, remover esses quantificadores.
Uma passagem possível seria de
para
A obtenção da forma conjuntiva normal/eliminar os símbolos e segue processos idênticos aos da Lógica Proposicional.
Unificação
Processo ligado à substituição. Permite determinar se duas fbfs atómicas podem ser tornadas iguais através de substituições apropriadas para as suas variáveis livres. Antes de considerar o problema da unificação, é relevante introduzir a composição de substituições.
Composição de substituições
Sendo e duas substituições, a composição destas, , é igual a tal que:
Colocado de forma formal, corresponde a:
A composição de substituições goza da propriedade associativa, mas não da comutativa.
Temos ainda que, e recuperando a noção de substituição vazia (), a composição com a substituição vazia é tal que .
Composição de Substituições - Exemplo
À primeira vista esta operação parece um "monstro", mas na verdade não tem nada que saber! A título de exemplo (e com ajuda de algumas cores), temos:
No fundo (e em linguagem corrente), devemos:
-
pegar em todos os termos de (à esquerda, portanto), e aplicar a substituição associada ao termo de (por exemplo, fica , visto que em existe a substituição ) - consideremos o termo resultante ; consideremos ainda que a variável original associada a cada substituição de , a azul, é dada por . A substituição resultante corresponde então a . Devemos, de seguida, aplicar esta lógica a todos os pares termo-variável de .
-
unir o conjunto acima obtido ao conjunto de pares termo-variável de em que a variável não está presente em : neste caso , já que apenas aparece em como termo (à esquerda), não como variável "substituível".
-
retirar todas as novas substituições que iam levar a termos iguais a variáveis - irrelevantes, portanto. Aqui, isso iria acontecer com a substituição , que como se pode observar abaixo leva a - uma substituição claramente irrelevante, e que pode portanto ser retirada.
O resultado final seria dado por:
Podemos ainda definir conjunto unificador: dado um conjunto de fbfs atómicas, este conjunto diz-se unificável caso exista uma substituição que torne idênticas todas as fbfs do conjunto, dizendo-se que essa substituição é um unificador do conjunto. Pode haver mais que um unificador para um dado conjunto.
A substituição é unificador do conjunto , dando origem a .
Existe ainda a noção de Unificador mais geral: dado um conjunto de fbfs atómicas, o unificador mais geral do conjunto, mgu, é um unificador com a seguinte propriedade:
- se for um unificador da fbf da qual é o mgu, então existe uma substituição tal que .
O mgu é único, exceto para variantes alfabéticas de variáveis.
Algoritmo de Unificação
Recebe um conjunto de fbfs atómicas e decide se podem ser unificadas, devolvendo o seu mgu. O algoritmo apresentado a seguir percorre, em paralelo, os constituintes desse conjunto (as fbfs a unificar), da esquerda para a direita, começando pelo mais à esquerda. À medida que vai encontrando constituintes diferentes, em desacordo, tenta determinar uma substituição que os torne iguais. Em caso de sucesso, o algoritmo continua a percorrer as fbfs que resultam da aplicação dessa substituição a todas as fbfs a unificar; caso contrário, termina, indicando que o conjunto não é unificável. Percorridas todas as fbfs, o algoritmo termina com sucesso e a composição das substituições encontradas corresponde ao mgu.
O algoritmo de unificação usa ainda outro algoritmo, o de desacordo, para determinar o conjunto de desacordo de um conjunto de fbfs. Obtém-se localizando o primeiro constituinte, a partir da esquerda, que não é igual a todas as fbfs do conjunto e extraindo das fbfs todos os componentes nessa posição.
Em , o conjunto de desacordo é : corresponde ao conjunto de fbfs em desacordo, que não são iguais em todas as fbfs de .
Exemplo de aplicação do Algoritmo de Unificação
Seja o conjunto . Se quisermos tentar determinar o seu mgu:
De cima para baixo, da esquerda para a direita:
Começamos por olhar para da esquerda para a direita; como podemos constatar,
e estão em desacordo, se considerarmos os primeiros argumentos de cada fbf.
Assim sendo, o conjunto atual de desacordo, , passa a ser . Sabemos que
deixa de ficar em desacordo se substituirmos por (a decisão é feita, mais uma vez,
ao ler da esquerda para a direita), e adicionamos, portanto essa mesma substituição
ao conjunto . Voltamos a verificar o conjunto de desacordo,
desta vez para o segundo argumento de cada fbf. Como é possível constatar, e
estão em desacordo. Contudo, ocorre em , pelo que a unificação não é
possível (originaria uma espécie de recursão infinita), e o algoritmo falha. O conjunto não é unificável.
Resolução
Podemos agora enunciar o princípio da resolução para o caso em que as cláusulas contêm variáveis.
Princípio da Resolução - caso geral
Sejam e duas cláusulas sem variáveis em comum, e e duas fbfs atómicas tais que e , e e são unificáveis, com o mgu destas. Segundo o princípio da resolução, podemos inferir a cláusula . Os literais e serão literais em conflito, e a cláusula obtida é o resolvente das cláusulas.
Em termos correntes, removemos os literais em conflito e aplicamos o mgu às que restam.
É, tal como a resolução da lógica proposicional, correta mas não completa. É, de igual forma, completa quanto à refutação.
Considere-se o seguinte exemplo, com:
O mgu de e é , e portanto o resolvente será a aplicação desse mesmo mgu à cláusula restante, obtendo .
Graficamente:
De notar que o resolvente pode não necessitar de uma substituição, isto é, pode existir resolvente entre duas cláusulas em que o conteúdo é "ele próprio" numa cláusula e a sua negação noutra, e aí podemos aplicar o resolvente tal como na lógica proposicional.
Renomeação de variáveis
Se repararmos, na definição é referida a necessidade de não haver variáveis em comum entre as fbfs. Esta necessidade pode ser satisfeita renomeando todas as variáveis das cláusulas relevantes antes da aplicação do princípio da resolução, por exemplo passar para . Esta renomeação apenas ocorre numa das cláusulas, a outra instância mantém-se intacta (podemos fazer isto porque, na verdade, estamos na presença de variáveis quantificadas universalmente, portanto mudas).
A título de exemplo, sejam e duas cláusulas. Para aplicar o princípio da resolução, temos antes de renomear as variáveis, renomeação essa que origina a cláusula . Sendo e duas variáveis diferentes, podemos agora unificá-las.
Porquê renomear as variáveis?
Consideremos a seguinte afirmação:
Na forma clausal, será
Se não renomearmos as variáveis, o mgu de e será , e a partir daí só podemos obter a cláusula . Por outro lado, se renomearmos as variáveis obtemos um mgu diferente e é possível chegar à expressão pretendida.
Este pormenor pode muitas vezes despercebido, mas é bastante importante (e é abordado em contexto de avaliação).
Como nota final, podemos afirmar que as noções de prova por resolução e refutação, bem como as estratégias de eliminação e seleção de cláusulas, migram da lógica proposicional para a de primeira ordem.