\documentclass[11pt,a4paper]{book}

\usepackage[brazil]{babel}
\usepackage[latin1] {inputenc}
\usepackage{fullpage}

\pagestyle{empty}

\begin{document}

\noindent Departamento de Ciência da Computa\c{c}\~{a}o \hfill ICEx/UFMG \\
\noindent {\it Lógica Aplicada a Computação} \hfill $\mbox{1}^{\mbox{\underline{o}}}$ semestre de 2013 \\
\noindent Professor: Newton José Vieira \\
\noindent {\bf Segundo Trabalho} \hfill Entrega: até 05/07/2011

\vspace*{8mm}
\noindent\textbf{\large Parte 1: Sat em Prolog}

\vspace*{5mm}
Implemente o algoritmo \textsf{satB-nd} (Figura 2.11) em Prolog. Utilize a diretiva {\tt op} para declarar operadores infixados para \textsf{nao}, \textsf{e}, \textsf{ou}, \textsf{imp}, \textsf{sse}. Use {\tt v} e {\tt f} para $\top$ e $\bot$, respectivamente. A seguir, alguns exemplos de interação com o programa, com uma interpretação que satisfaça uma fórmula coletada em uma lista:

\begin{verbatim}
?- sat((p e nao p) imp f,I).
I = [[p, f]] ;
I = [[p, v]] ;
false.

?- sat((p ou q) e nao p imp q,I).
I = [[q, f], [p, f]] ;
I = [[p, v]] ;
I = [[q, v]] ;
false.

?- sat(nao ((p ou q) e nao p imp q),I).
false.

?- sat((p imp q) e ((q ou r) imp p),I).
I = [[r, f], [q, f], [p, f]] ;
I = [[p, v], [q, v]] ;
false.
\end{verbatim}

\noindent Note que são fornecidas as interpretações uma a uma, sob solicitação. \emph{Dicas}:
\begin{itemize}
 \item Indique no programa que constantes são variáveis (via uma lista).
 \item Programe um predicado auxiliar {\tt satac(Frm,I1,I2)} que, recebendo como entradas a fórmula {\tt Frm} e
       a interpretação (até o momento) {\tt I1}, dê como resultado a interpretação {\tt I2}. Com isso, o programa
			 teria a seguinte regra:
			\begin{verbatim} sat(Frm,I) :- satac(Frm,[],I). \end{verbatim}
 \item O não determinismo pode ser deixado por conta do mecanismo de controle de Prolog. Por exemplo:
			\begin{verbatim}
	 satac(Subf1 ou Subf2,I1,I2) :- satac(Subf1,I1,I2) ; satac(Subf2,I1,I2).
	 satac(Subf1 e  Subf2,I1,I3) :- satac(Subf1,I1,I2) , satac(Subf2,I2,I3).
			\end{verbatim}
\end{itemize}

\pagebreak

\noindent\textbf{\large Parte 2: FNC em Prolog}

\vspace*{5mm}
Implemente o algoritmo \textsf{fnc} (Figura 2.37) em Prolog. Utilize as mesmas diretivas {\tt op} da parte anterior para declarar operadores infixados para \textsf{nao}, \textsf{e}, \textsf{ou}, \textsf{imp}, \textsf{sse}. Não há necessidade de simplicar a FNC obtida.  A seguir, alguns exemplos do que seria uma interação com o programa:

\begin{verbatim}
?- fnc((nao p e q) ou p,X).
X = [[nao p, p], [q, p]] ;
false.

?- fnc(nao(p imp q) ou (nao p e r),X).
X = [[p, nao p], [p, r], [nao q, nao p], [nao q, r]] ;
false.

?- fnc((nao(q ou r) imp p)  ou (nao p imp q),X).
X = [[q, r, p, p, q]] ;
false.

?- fnc(p sse (q ou (nao p e r)),X).
X = [[nao p, q, nao p], [nao p, q, r], [p, nao q], [p, p, nao r]] ;
false.
\end{verbatim}

\end{document}
 

