SBC_Lista_2.pdf

SBC_Lista_2.tex

\documentclass{article}

\usepackage{lmodern}
\usepackage[]{algorithm2e}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[portuguese]{babel}
\usepackage{mathtools}
\usepackage{enumitem}
\usepackage{listings}

\title{Lista 2 de Sistemas Baseados em Conhecimento}
\author{9410313 - Walter Perez Urcia}

\begin{document}

\maketitle

\section{Exercício 1}
	\subsection{Declaração}
		Explique com suas palavras por que a regra de inferência abaixo, chamada resolução, é sempre correta
			\[ c_1 \cup \{ p \} , c_2 \cup \{ \lnot p \} \vdash c_1 \cup c_2 \]
		onde $c_1$ e $c_2$ são cláusulas e $p$ um literal.\\
		Obs: Lembre que uma cláusula é um conjunto de literais, interpretado como sua disjunção.
	\subsection{Solução}
		Aquela regra de inferência é sempre correta porque se $p$ é verdadeiro, a cláusula $c_2$ tem que ser verdadeira para que o conjunto de cláusulas seja verdadeiro. Da mesma forma, se $p$ é falso, a cláusula $c_1$ tem que ser verdadeira. Portanto, para qualquer valor de $p$ (verdadeiro ou falso), tem que ser verdadeiro $c_1 \cup c_2$.

\section{Exercício 2}
	\subsection{Declaração}
		Resolução é um método de inferência correto? E completo? É completo para refutação? Explique o que essas afirmações significam.
	\subsection{Solução}
		Como se mostrou na solução anterior, resolução é um método de inferência correto. Resolução é completa para refutação porque para qualquer conjunto $S$, só é verdade que $S \rightarrow []$ se e solo se $S \models []$. Mas não é completa para outros casos, porque só é verdade que $S \rightarrow c \implies S \models c$, mas o contrario não ($S \models c \implies S \rightarrow c$). Por exemplo, $S = \{ [ \lnot p ] \}$ e $c = [ \lnot p , \lnot q ]$ é verdade que $S \models c$, mas não existe uma derivação possível para $c$.

\section{Exercício 3}
	\subsection{Declaração}
		Formalize as seguintes sentenças usando os predicados unários ${fezEx}$, ${vaiBem}$, ${mediaAlta}$ e o predicado binário ${aprovado}$:\\
		"Quem fez os exercícios vai bem na prova"\\
		"Quem vai bem na prova fica com média alta"\\
		"Quem fica com média alta é aprovado em mac444"\\
		"João fez os exercícios"\\
		"Maria foi bem na prova"\\
		Use resolução SLD para mostrar que João e Maria foram aprovados em mac444.
	\subsection{Solução}
		Formalizando as sentenças com predicados temos:
		\begin{itemize}
			\item $\forall x , {fezEx}( x ) \implies {vaiBem}( x )$
			\item $\forall x , {vaiBem}( x ) \implies {mediaAlta}( x )$
			\item $\forall x , {mediaAlta}( x ) \implies {aprovado}( x , mac444 )$
			\item ${fezEx}( J )$
			\item ${vaiBem}( M )$
		\end{itemize}
		Onde $J = \text{João}$ e $M = \text{Maria}$. Então a base de conhecimento $S$ será:
		\begin{itemize}
			\item $[ \lnot {fezEx}( x ) , {vaiBem}( x ) ]$
			\item $[ \lnot {vaiBem}( x ) , {mediaAlta}( x ) ]$
			\item $[ \lnot {mediaAlta}( x ) , {aprovado}( x , mac444 ) ]$
			\item $[ {fezEx}( J ) ]$
			\item $[ {vaiBem}( M ) ]$
		\end{itemize}
		Queremos mostrar $S \vdash \alpha$, onde $\alpha = {aprovado}( J , mac444 ) \land {aprovado}( M , mac444 )$. Então temos que mostrar que $S \land \lnot \alpha$ é insatisfatível. Usando resolução SLD temos:
		\begin{enumerate}
			\item $[ \lnot {aprovado}( J , mac444 ) , \lnot {aprovado}( M , mac444 ) ]$ com\\
				$[ \lnot {mediaAlta}( x ) , {aprovado}( x , mac444 ) ]\{x/M\} \vdash$\\
				$[ \lnot {mediaAlta}( M ) , \lnot {aprovado}( J , mac444 ) ]$
			\item $[ \lnot {mediaAlta}( M ) , \lnot {aprovado}( J , mac444 ) ]$ com\\
				$[ \lnot {vaiBem}( x ) , {mediaAlta}( x ) ]\{x/M\} \vdash$\\
				$[ \lnot {vaiBem}( M ) , \lnot {aprovado}( J , mac44 ) ]$
			\item $[ \lnot {vaiBem}( M ) , \lnot {aprovado}( J , mac44 ) ]$ com\\
				$[ {vaiBem}( M ) ] \vdash$\\
				$[ \lnot {aprovado}( J , mac444 ) ]$
			\item $[ \lnot {aprovado}( J , mac444 ) ]$ com\\
				$[ \lnot {mediaAlta}( x ) , {aprovado}( x , mac444 ) ]\{ x/J \} \vdash$\\
				$[ \lnot {mediaAlta}( J ) ]$
			\item $[ \lnot {mediaAlta}( J ) ]$ com\\
				$[ \lnot {vaiBem}( x ) , {mediaAlta}( x ) ]\{ x/J \} \vdash$\\
				$[ \lnot {vaiBem}( J ) ]$
			\item $[ \lnot {vaiBem}( J ) ]$ com\\
				$[ \lnot {fezEx}( x ) , {vaiBem}( x ) ]\{ x/J \} \vdash$\\
				$[ \lnot {fezEx}( J ) ]$
			\item $[ \lnot {fezEx}( J ) ]$ com\\
				$[ {fezEx}( J ) ] \vdash$\\
				$[]$
		\end{enumerate}
		Portanto, foi mostrado que $S \models \alpha$ usando resolução SLD.

\section{Exercício 4}
	\subsection{Declaração}
		Quais as diferenças no proceso de resolução para lógica proposicional e para lógica de primeira ordem?
	\subsection{Solução}
		Na lógica proposicional as cláusulas não tem variáveis na base de conhecimento, mas na lógica de primeira ordem as cláusulas podem conter variáveis. Devido a isso, para lógica de primeira ordem tem que ser feitas substituições das variáveis nas cláusulas da inferência (em alguns casos) em cada paso de resolução. Além disso, podem ser usadas cláusulas com variáveis sem fazer substituições se fosse possível (em caso uma tenha $P( x )$ e a outra $\lnot P( x )$). Por último, na lógica de primeira ordem, a resolução pode ser usada para encontrar a resposta (ou respostas) a um query na base de conhecimento adicionando literais com as variáveis desejadas sem substituir.

\section{Exercício 5}
	\subsection{Declaração}
		A skolemização gera uma fórmula que não é logicamente equivalente à original. Explique por que a resolução funciona mesmo assim (isto é, continua sendo correta)
	\subsection{Solução}
		Skolemização funciona porque apesar que não gera uma fórmula $\alpha'$ logicamente equivalente a $\alpha$, a fórmula gerada faz que a base fique satisfatível ou insatisfatível do mesmo jeito que $\alpha$. O anterior é suficiente para que resolução seja usada corretamente.

\section{Exercício 6}
	\subsection{Declaração}
		O que são cláusulas de Horn e por que elas são úteis para o proceso de resolução?
	\subsection{Solução}
		As cláusulas de Horn são aquelas que tem como máximo um literal positivo. Uma cláusula de Horn é chamada negativa ($N$) se todos seus literais são negações ou é vazia e positiva ($P$) se tem só um literal positivo. São úteis para o proceso de resolução porque reduz as posibilidades de escolher cláusulas a aquelas da forma $N + P = N$ e $P + P = P$. Além disso, se fazemos que todas as cláusulas derivadas sejam negativas, então só temos o primer caso sendo um pai positivo e o outro negativo, de ese jeito a cláusula derivada (negativa) pode ser um novo pai para outra cláusula negativa.

\end{document}