WorksheetsUnificação e resolução
Total questions: 15
Worksheet time: 10mins
O que é um unificador em para conjunto de cláusulas {A,B,C,…}?
Uma substituição que torna todas as cláusulas idênticas.
Uma substituição que remove todas as variáveis das cláusulas.
Uma substituição que remove todas as variáveis das cláusulas.
O que é um conjunto de desacordo no contexto do algoritmo de unificação?
As variáveis que não podem ser substituídas.
As substituições que devem ser feitas para unificar os termos.
As substituições que devem ser feitas para unificar os termos.
Qual das seguintes condições é necessária para uma substituição válida θ={t1/v1,t2/v2,…,tn/vn}θ={t1/v1,t2/v2,…,tn/vn}?
Cada termo ti deve ser igual à variável vi.
Nenhum termo ti pode conter a variável vi (evitar ciclos).
Todas as variáveis vi devem ser iguais entre si.
Seja a substituição composta θ1∘θ2={f(b)/X,b/Y,Z/U}. Qual das opções abaixo poderia representar θ1 e θ2 originalmente?
θ1={f(Y)/X, U/Z},
θ2={b/Y, Z/U}
θ1={a/X,b/Y}, θ2={f(a)/X}
θ1={X/Y},
θ2={Y/X}
Um conjunto de expressões é considerado não unificável quando:
Contém constantes diferentes em posições correspondentes.
Uma variável precisa ser substituída por um termo que a contém (ex: X por f(X)).
Ambas as opções anteriores estão corretas.
O que é um resolvente na regra de resolução?
Uma nova cláusula gerada pela união de duas cláusulas-pais sem literais complementares.
Uma nova cláusula gerada pela união de duas cláusulas-pais sem literais complementares.
Uma fórmula na Forma Normal Conjuntiva (FNC) simplificada.
Qual é o resolvente das cláusulas ∼p∨q e p?
q
∼p∨q
p∨q
Na prova por resolução, o que representa a obtenção de uma "cláusula vazia"?
Uma tautologia.
Uma contradição (absurdo).
Uma fórmula indeterminada.
Qual é a Forma Normal Conjuntiva (FNC) de ∼p→q
p∨q
∼p∨∼q
p∧q
O que é Skolemização?
Remoção de quantificadores universais substituindo variáveis por constantes.
Eliminação de quantificadores existenciais usando constantes ou funções de Skolem.
Conversão de fórmulas para Forma Normal Prenex sem alterar quantificadores.
Qual substituição unifica P(w,x) e ∼P(y,z)?
{w/y,x/z}
{y/w,z/x}
{w/x,y/z}
Qual é o resultado da resolução entre ∼p∨q∨r e ∼q∨∼r?
∼p∨q∨∼q
∼p∨∼r∨r
Ambas as opções anteriores estão corretas.
Na Forma Normal Prenex, onde devem estar os quantificadores?
No final da fórmula.
No início da fórmula.
Distribuídos entre os literais.
Qual é a vantagem da prova por resolução?
Requer múltiplas regras de inferência.
Tudo se resume a aplicar uma única regra (a resolução).
Não exige conversão para FNC.
Qual é o propósito principal da Skolemização na lógica de predicados?
Introduzir novos quantificadores existenciais para tornar a fórmula mais expressiva.
Eliminar quantificadores existenciais substituindo variáveis por constantes ou funções de Skolem, permitindo a aplicação da resolução.
Converter todos os quantificadores universais em quantificadores existenciais para simplificação.
