|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2010-proj-pesq.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-proj-pesq.tex && latex 2010-proj-pesq.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-proj-pesq.tex && pdflatex 2010-proj-pesq.tex"))
% (eev "cd ~/LATEX/ && Scp 2010-proj-pesq.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010-proj-pesq.dvi"))
% (find-dvipage "~/LATEX/2010-proj-pesq.dvi")
% (find-pspage "~/LATEX/2010-proj-pesq.pdf")
% (find-pspage "~/LATEX/2010-proj-pesq.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010-proj-pesq.ps 2010-proj-pesq.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010-proj-pesq.ps 2010-proj-pesq.dvi && ps2pdf 2010-proj-pesq.ps 2010-proj-pesq.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010-proj-pesq.pdf" (ee-twupfile "LATEX/2010-proj-pesq.pdf") 'over)
% (ee-cp "~/LATEX/2010-proj-pesq.pdf" (ee-twusfile "LATEX/2010-proj-pesq.pdf") 'over)
\documentclass[a4paper,12pt,titlepage]{article}
\usepackage[brazil]{babel}
% \usepackage[latin1]{inputenc}
% \usepackage[T1]{fontenc}
% \documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\usepackage{amssymb,amsmath,amsthm}
\usepackage{babelbib}
\usepackage{url}
\usepackage{ifthen}
\usepackage{rotating}
\newcommand{\hoje}{9 de março de 2007}
\newcommand{\x}{\ensuremath{\surd}}
\newcommand{\cronentry}[1]{\raggedright\rule{0ex}{4ex}#1\rule[-2.5ex]{0ex}{4ex}}
% \begin{document}
\input 2010-proj-pesq.dnt
%*
% (eedn4-51-bounded)
%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
%*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Arrays with numbered lines (specs) --- by fnaufel@gmail.com
% (requires ifthen package)
%
% For some weird reason, labeling does not work if \spec appears
% in math mode \[ \] when package amsmath is used.
%
% However, it works ok with amsmath and $$...$$.
%
% But \spec can be used outside of math mode. If centering is desired,
% use \begin{center}...\end{center}.
%
% Finally, it works with \boxed{} and amsmath.
%
% For centered, boxed specs, use \begin{center}\fbox{...}\end{center}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newboolean{numberspec}
\setboolean{numberspec}{false}
\newcounter{specline}
\newcommand{\nl}{\tabularnewline\numberedline}
\newcommand{\numberedline}{%
\ifthenelse{\boolean{numberspec}}%
{%
\refstepcounter{specline}%
\ifthenelse{\value{specline} < 10}%
{\mbox{\small\phantom{0}\thespecline}\quad}%
{\mbox{\small\thespecline}\quad}%
}%
{\quad}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The command \spec:
%
% Args:
% 1 - optional [nonumbers]
% 2 - name (first line)
% 3 - body
\newcommand{\spec}[3][{}]{%
\setcounter{specline}{0}%
\ifthenelse{\equal{#1}{numbers}}%
{\setboolean{numberspec}{true}}%
{\setboolean{numberspec}{false}}%
\ensuremath{
\begin{array}{l}
\ifthenelse{\equal{#2}{}}
{\numberedline}
{#2\nl}
#3
\end{array}
}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Notes to myself:
\newcommand{\nota}[1]{
\marginpar{
\em \tiny
\begin{flushleft}
#1
\end{flushleft}
}
}
\newcommand{\att}[2]{
\begin{center}
\vskip 1ex
\noindent
\fbox{
\parbox{0.9\linewidth}{
\begin{center}
\bf #1
\end{center}
#2
\vskip 1ex
}
}
\vskip 1ex
\end{center}
}
\newcommand{\outline}[1]{\att{Esboço}{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% DL:
\newcommand{\dland}{\sqcap} % concept intersection
\newcommand{\dlor}{\sqcup} % concept union
\newcommand{\subs}{\sqsubseteq} % concept subsumption
\newcommand{\conc}{\textit} % concept name
\newcommand{\role}{\textit} % role name
\newcommand{\alc}{\ensuremath{\mathcal{ALC}}}
\newcommand{\pspace}{\textsc{PSpace}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
\title{%
Projeto de Pesquisa:\\
Explicando Provas
em Lógicas de Descrição
}
\author{%
Prof.\ Fernando Náufel do Amaral\\
Matr.\ UFF 01312630 \quad Matr.\ SIAPE 2295783\\
Ciência da Computação\\
DCT -- Depto.\ de Ciência e Tecnologia\\
PURO -- Pólo Universitário de Rio das Ostras\\
UFF -- Universidade Federal Fluminense%
}
\date{\hoje}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\begin{document}
\maketitle
\begin{abstract}
Este projeto visa estudar maneiras de apresentar e explicar provas formais em lógicas de descrição (DL) a usuários sem treinamento específico em lógica ou dedução automática. Para tanto, aborda tanto questões relativas à construção de provas em diferentes cálculos dedutivos para DL quanto questões relativas à estruturação e à apresentação das explicações.
\end{abstract}
\tableofcontents
\newpage
\section{Descrição do Problema}
\label{sec-descr}
\subsection{Lógicas de Descrição (DL)}
\label{sec-DL}
DL (\emph{Description Logics})~\cite{DLHandbook} é um termo que se refere a diversas linguagens lógicas frequentemente usadas para representação de conhecimento em Inteligência Artificial. Tais linguagens se originam de formalismos de representação de conhecimento da década de 1970, como redes semânticas e quadros (\emph{frames}).
Atualmente há, por parte da comunidade científica, um grande interesse em DL por causa da importância destas linguagens lógicas no desenvolvimento da chamada \emph{Web Semântica}~\cite{tblSciAm, tblIEEE}, onde enormes bases de conhecimento, de procedências diversas, estarão disponíveis na rede para serem consultadas e manipuladas por agentes inteligentes de \emph{software}. De fato, a linguagem OWL (\emph{Web Ontology Language})~\cite{owlWeb} fornece a DL uma sintaxe ao estilo XML, visando a integração destas lógicas com as ferramentas e os formalismos mais comuns na WWW; satisfeitas certas restrições, uma ontologia escrita em OWL corresponde exatamente a uma teoria em~DL. Para que os agentes de \emph{software} que acessam tais ontologias possam se comunicar entre si e conciliar diferentes visões de mundo, eles devem ser capazes de compreender diferentes formas nas quais pode se representar o conhecimento e de retirar conclusões a partir das informações encontradas, tarefas para as quais DL e seus mecanismos de inferência são adequados.
Em DL, \emph{termos de conceitos} descrevem classes de indivíduos em algum universo, enquanto \emph{termos de papéis} (também chamados de \emph{propriedades}) representam relações binárias ligando indivíduos. Para os nossos propósitos, a sintaxe de conceitos e propriedades é definida pela gramática
\[
\begin{array}{rcll}
C, D & \to & A & \textrm{(conceito atômico)} \\
& \mid & \top & \textrm{(conceito universal)} \\
& \mid & \bot & \textrm{(conceito vazio)} \\
& \mid & \neg C & \textrm{(negação)} \\
& \mid & C \dland D & \textrm{(interseção)} \\
& \mid & C \dlor D & \textrm{(união)} \\
& \mid & \forall R.C & \textrm{(restrição de valor)} \\
& \mid & \exists R.C & \textrm{(quantificação existencial)} \\
\end{array}
\]
onde $R$ representa nomes atômicos de papéis (o único tipo de termo de papel). Esta sintaxe corresponde à linguagem lógica conhecida como \alc.
Uma das maneiras usuais de interpretar termos de conceitos consiste em traduzi-los para expressões de teoria dos conjuntos. Formalmente, define-se uma interpretação como sendo um mapeamento $\mathcal{I}$ de termos de conceitos para conjuntos de indivíduos de um universo $\Delta$ e de termos de papéis para relações binárias sobre $\Delta$ satisfazendo as seguintes condições:
\[
\begin{array}{rcl}
\mathcal{I}(\top) & = & \Delta \\
\mathcal{I}(\bot) & = & \varnothing \\
\mathcal{I}(\neg C) & = & \Delta - \mathcal{I}(C) \\
\mathcal{I}(C \dland D) & = & \mathcal{I}(C) \cap \mathcal{I}(D) \\
\mathcal{I}(C \dlor D) & = & \mathcal{I}(C) \cup \mathcal{I}(D) \\
\mathcal{I}(\forall R.C) & = & \{ a \in \Delta \mid \forall b. [(a,b) \in
\mathcal{I}(R) \Rightarrow b \in \mathcal{I}(C)] \} \\
\mathcal{I}(\exists R.C) & = & \{ a \in \Delta \mid \exists b. [(a,b) \in
\mathcal{I}(R) \land b \in \mathcal{I}(C)] \} \\
\end{array}
\]
Se um indivíduo $a$ pertence ao conjunto representado por um termo de conceito $C$, dizemos que $a$ \emph{está em} $C$. Se um par $(a, b)$ de indivíduos pertence à relação binária representada por $R$, dizemos que $b$ \emph{preenche a propriedade $R$ de} $a$, ou que $b$ \emph{é um preenchedor de} $R$.
Informalmente, um termo de conceito da forma $\forall R.C$ representa o conjunto de todos os indivíduos que possuem todos os preenchedores de $R$ (caso existam) em $C$. Um termo de conceito da forma $\exists R.C$ representa o conjunto de todos os indivíduos que possuem pelo menos um preenchedor de $R$ em $C$.
Em DL, uma fórmula de \emph{subsunção}, escrita $C \subs D$, representa o enunciado de que a classe denotada por $C$ está contida na classe denotada por $D$. Uma fórmula de \emph{equivalência} $C \equiv D$ representa o enunciado de que $C$ subsume $D$ e $D$ subsume $C$; i.e., $C$ e $D$ denotam a mesma classe.
Uma \emph{TBox} (de \emph{terminologia}) é uma coleção de fórmulas de subsunção e/ou equivalência em DL tomadas como axiomas. Em outras palavras, uma \emph{TBox} é uma \emph{teoria} na linguagem de DL. O processo de \emph{inferência} ou \emph{dedução} consiste em descobrir que fórmulas de DL são consequências lógicas de uma \emph{TBox} $T$.
\subsection{Dedução Automática em DL}
\label{sec-deducaoDL}
A área de \emph{prova automática de teoremas}, ou \emph{dedução automática}, ou \emph{inferência automática} \cite{darURL}, lida com o desenvolvimento de algoritmos que decidem se uma dada fórmula de entrada, expressa em uma determinada linguagem lógica, é consequência lógica de uma dada teoria (conjunto de axiomas e premissas).
No caso específico de DL, como visto na Seção~\ref{sec-DL}, a fórmula de entrada pode ser uma subsunção ($C \subs D$) ou uma equivalência ($C \equiv D$). Dependendo dos termos de conceitos $C$ e $D$ envolvidos, fórmulas de subsunção podem ter significados diversos. Em especial, dada uma \emph{TBox} $T$,
\begin{itemize}
\item Se a subsunção $C \subs \bot$ é consequência lógica de $T$, dizemos que $C$ representa um conceito \emph{insatisfatível} em $T$. Isto significa que, segundo os axiomas de $T$, é impossível existir qualquer indivíduo que satisfaça a descrição do conceito $C$. No contexto de modelagem conceitual~\cite{calvaneseCDM}, um conceito insatisfatível frequentemente indica alguma inconsistência na construção do modelo.
\item Se as subsunções $C \subs D$ e $D \subs C$ são consequências lógicas de $T$, podemos concluir que $C \equiv D$ também o é.
\item Se o conceito $C \dland D$ for insatisfatível em $T$ (i.e., se $C \dland D \subs \bot$ for consequência lógica de $T$), dizemos que $C$ e $D$ são \emph{disjuntos} em $T$, o que significa que nenhum indivíduo pode satisfazer, simultaneamente, as descrições de $C$ e de $D$.
\end{itemize}
Estas observações significam que estes três tipos de consultas importantes em~DL (insatisfatibilidade, equivalência e disjunção de conceitos) são redutíveis à subsunção. Portanto, a principal tarefa de inferência oferecida por provadores automáticos de DL é justamente verificar se uma fórmula de subsunção é consequência lógica de uma \emph{TBox}.
Uma ontologia contém, entre outras informações, uma \emph{hierarquia} (ou \emph{taxonomia}) dos conceitos presentes no domínio modelado. Esta hierarquia organiza os conceitos segundo as relações de subsunção entre eles. Ao construir uma ontologia, um engenheiro de conhecimento enuncia \emph{explicitamente} as relações de subsunção que ele deseja que valham entre os conceitos definidos. No entanto, frequentemente ocorre que a ontologia construída também define, \emph{implicitamente}, outras relações de subsunção, consequências lógicas dos axiomas escritos pelo engenheiro de conhecimento. O processo de descoberta (via inferência) destas subsunções implícitas se denomina \emph{classificação} da ontologia, e é mais uma indicação da importância das consultas de subsunções em DL.
Cabe ressaltar, neste ponto, que a tarefa de verificar se uma dada fórmula de DL\footnote{
Observe que estamos nos restringindo à linguagem de \alc, definida na Seção~\ref{sec-DL}.
}
é consequência de uma dada \emph{TBox} é um problema \emph{decidível}~\cite[cap.~2]{DLHandbook}, ao contrário do que ocorre com a tarefa análoga em Lógica de Primeira Ordem, por exemplo. Isto significa que qualquer consulta sobre uma dada subsunção com respeito a uma dada \emph{TBox} pode ser respondida algoritmicamente em tempo finito. No que tange à dificuldade deste problema, porém, observamos que as complexidades de tempo e de espaço da tarefa de inferência em~DL variam segundo a expressividade da linguagem (i.e., os construtores de termos de conceitos e de papéis permitidos). No caso específico de \alc, inferência é um problema \pspace-difícil~\cite[cap.~3]{DLHandbook}. Este fato torna necessário que os algoritmos de inferência para~DL utilizem técnicas heurísticas para tentar evitar elevados tempos de resposta.
Inicialmente, os provadores de teoremas de DL usavam algoritmos de subsunção estrutural para provar fórmulas de linguagens menos expressivas que \alc. Tais algoritmos consistiam basicamente em (1) reduzir os conceitos envolvidos em uma fórmula de subsunção a suas formas normais e (2) comparar as estruturas destas formas normais. Para linguagens que, como \alc, contêm conceitos construídos com negação de conceitos arbitrários e disjunção, esta estratégia não é completa. Atualmente, os principais algoritmos de inferência em~DL implementam cálculos dedutivos baseados em \emph{tableaux}~\cite{baaderOverview}. Entre as implementações mais importantes, destacamos os provadores Pellet~\cite{pellet} (livre e gratuito) e Racer~\cite{racer} (comercial). No que diz respeito à apresentação de provas ao usuário, os cálculos baseados em \emph{tableaux} costumam produzir provas de pouca legibilidade, uma característica que, no caso específico de~DL, é agravada pelo uso das técnicas heurísticas mencionadas acima. Uma das metas do presente projeto de pesquisa é estudar estes cálculos dedutivos para~DL (e suas implementações) do ponto de vista da apresentação de provas para o usuário.
Naturalmente, dada uma \emph{TBox} $T$ e uma subsunção $C \subs D$, pode ocorrer que a subsunção \emph{não seja} consequência lógica de $T$. Neste caso, nenhum provador conseguirá construir uma prova desta fórmula a partir de $T$, pois tal prova não existe. No que tange à interação com o usuário, pode ser interessante que o provador apresente alguma explicação desta inexistência, talvez na forma de um registro da tentativa malsucedida de construção da prova, com a indicação dos passos em que tal tentativa fracassou. A apresentação e a explicação de tentativas malsucedidas de provas são recursos importantes, por exemplo, para o engenheiro de conhecimento durante a fase de construção de uma ontologia, servindo como testes de ``depuração'' do conhecimento que já se encontra formalizado.
\subsection{Explicação de Provas}
Explicações constituem assunto de pesquisa de diversas disciplinas, incluindo, por exemplo, Filosofia da Ciência, Matemática, Lingüística e Inteligência Artificial. Esta diversidade aponta para a existência de diferentes visões sobre o que exatamente vem a ser uma explicação. No nosso caso, estamos interessados em explicações de provas em~DL, mas a \emph{natureza} e a \emph{forma} de tais explicações são questões em aberto. Mencionamos algumas possibilidades:
\begin{itemize}
\item Uma prova em um cálculo dedutivo baseado em \emph{tableaux} é usualmente representada por uma árvore cujos nós são rotulados por fórmulas. A simples apresentação desta árvore poderia ser considerada uma explicação (ainda que bem rudimentar) da conclusão da prova;
\item A mesma árvore descrita no item anterior, com as fórmulas dos nós e a conclusão parafraseadas em linguagem natural, ofereceria uma legibilidade maior para usuários leigos;
\item Caso a árvore correspondente à prova seja muito grande, recursos gráficos e de hipertexto poderiam ser utilizados para apresentar partes da prova ao usuário de forma interativa;
\item Em vez de pressupor que o usuário seja capaz de compreender a estrutura da prova em um cálculo dedutivo específico (e.g., \emph{tableaux}), a prova inteira poderia ser traduzida para linguagem natural, onde as regras de inferência específicas do cálculo dariam lugar a padrões lingüísticos comuns em argumentações em prosa;
\item Alternativamente, o cálculo dedutivo utilizado na prova poderia ser traduzido para algum formalismo gráfico cujo entendimento seja mais intuitivo para um usuário não treinado em lógicas e dedução automática.
\end{itemize}
Apesar de usarmos a expressão ``explicação de provas'', ressaltamos na Seção~\ref{sec-deducaoDL} que também pode ser necessário explicar por que uma determinada fórmula \emph{não é} consequência lógica de uma \emph{TBox}. Neste caso, apontamos algumas alternativas:
\begin{itemize}
\item Apresentar um ``contra-exemplo''. No contexto específico de~DL, isto significa exibir um modelo que satisfaça os axiomas da \emph{TBox} dada mas não satisfaça a fórmula que se desejava provar;
\item Apresentar uma ``prova parcial'', com algum tipo de indicação dos motivos pelos quais ela não pode ser completada.
\end{itemize}
O estudo de explicações de provas em DL se iniciou com o trabalho~\cite{mcGuinness95}, onde provas construídas por um algoritmo de subsunção estrutural em uma linguagem menos expressiva que \alc{} são explicadas de forma modular, permitindo que o usuário decomponha raciocínios longos em seqüências mais curtas de passos e receba explicações destas seqüências. Posteriormente, o trabalho foi estendido em~\cite{borgida1999, borgida2000} para comportar provas de fórmulas na linguagem \alc. Outras linhas de pesquisa, como~\cite{parsia2005, schlobach2003}, visam desenvolver algoritmos específicos (não propriamente cálculos dedutivos) para localizar conceitos inconsistentes em ontologias e rastrear a origem destas inconsistências. Alguns outros trabalhos, como~\cite{meier2000}, usam a estratégia de traduzir fórmulas de DL para outras lógicas (e.g., modais ou de primeira ordem) e construir (e explicar) provas das fórmulas traduzidas, com base em cálculos dedutivos de uso comum nestas outras lógicas (e.g., seqüentes ou resolução).
\section{Objetivos}
\label{sec-obj}
\subsection{Objetivo Geral}
\begin{itemize}
\item Desenvolver técnicas para apresentar e explicar provas (e tentativas malsucedidas de provas) em DL para usuários sem conhecimentos específicos de lógica e dedução automática.
\end{itemize}
\subsection{Objetivos Específicos}
\begin{itemize}
\item Estudar cálculos dedutivos existentes para DL do ponto de vista da adequação à geração de explicações de provas.
\item Definir, se necessário e viável, um novo cálculo dedutivo para DL que reúna as vantagens apresentadas pelos cálculos estudados.
\item No caso da definição de um novo cálculo dedutivo para DL, provar sua correção e completude.
\item Desenvolver técnicas para a geração de explicações a partir de (tentativas~de)~provas no cálculo dedutivo adotado.
\item Definir uma notação, baseada em linguagem natural e/ou diagramas, para apresentar as explicações geradas.
\end{itemize}
\section{Metodologia}
\label{sec-metod}
Este projeto pretende envolver, além do pesquisador proponente, uma equipe de dois ou mais alunos de Ciência da Computação, na qualidade de bolsistas de iniciação científica, conforme detalhado abaixo, na Seção~\ref{sec-equipe}. A metodologia a ser empregada leva em consideração aspectos pedagógicos relativos à motivação e ao aprendizado dos alunos participantes, visando apresentar-lhes o universo da pesquisa teórica e aplicada em Lógica e Representação de Conhecimento. Em especial, fases de estudo teórico devem ser intercaladas com fases de implementação e utilização de ferramentas computacionais (ver cronograma abaixo, na Seção~\ref{sec-cron}), cabendo lembrar que, em se tratando de um projeto de pesquisa --- e não de desenvolvimento --- as ferramentas implementadas pela equipe constituirão apenas protótipos e provas de princípios (ao invés de produtos acabados).
Além de participar de apresentações de questões e resultados em seminários internos, a equipe deverá interagir com pesquisadores e alunos de pós-graduação do Laboratório de Técnicas e Métodos Formais (TecMF) do Departamento de Informática da PUC-Rio, onde existem projetos de pesquisa em tópicos relacionados a~DL e aplicações a Representação de Conhecimento. Esta interação interinstitucional, que deverá se dar através de encontros informais e de um ou mais \emph{workshops} do projeto, enriquecerá a experiência dos alunos bolsistas e contribuirá para uma maior sinergia nos resultados alcançados.
Obtidos resultados parciais sobre explicação de provas e desenvolvidos protótipos de ferramentas de \emph{software}, planejamos realizar estudos empíricos envolvendo usuários de diferentes procedências e formações para avaliar a adequação, em termos de legibilidade e usabilidade, das explicações geradas.
Finalmente, esperamos divulgar os resultados obtidos no projeto em eventos e periódicos adequados, conforme detalhado na Seção~\ref{sec-benef} abaixo, obtendo avaliações e sugestões de outros pesquisadores da área.
\section{Benefícios Esperados}
\label{sec-benef}
\begin{description}
\item [Relacionamento com PLN:] A área de Processamento de Linguagem Natural (PLN) possui ligações significativas com este projeto: por um lado, uma das formas cogitadas para apresentar explicações de provas é textual; por outro lado, conforme relatado em trabalho de autoria do pesquisador proponente e outros \cite{vorte2006}, é possível utilizar DL para formalizar a semântica de textos em linguagem natural e, posteriormente, empregar provadores de teoremas para raciocinar sobre a informação contida nos textos originais. O trabalho citado \cite{vorte2006} apresenta resultados preliminares desta estratégia no contexto da formalização de textos normativos sobre governança de segurança da informação.
Um dos resultados previstos deste projeto é o esclarecimento e a exploração dos relacionamentos entre DL e a semântica de textos em linguagem natural. Em especial, esperamos definir maneiras de utilizar elementos sintáticos do texto original para construir explicações textuais de provas sobre o conteúdo deste mesmo texto, tornando as explicações mais naturais e legíveis.
\item [Cálculos dedutivos para DL:] Prevemos a necessidade de definir novos cálculos dedutivos para DL, que se afastem do padrão atual de algoritmos baseados em \emph{tableaux}. Acreditamos que tal padrão se estabeleceu por causa do desejo de obter provadores eficientes, mas as provas construídas podem não se prestar facilmente à geração de explicações para o usuário.
Entre os produtos deste projeto, esperamos obter ou (1) uma maneira eficaz de traduzir provas em \emph{tableaux} para algum formalismo mais propício à geração de explicações, ou (2) um cálculo dedutivo totalmente novo, que reúna, na medida do possível, a eficiência dos cálculos baseados em \emph{tableaux} com a adequação à geração de explicações.
\item [Formação de grupo de pesquisa:] Este projeto servirá para estabelecer um grupo de pesquisa interinstitucional envolvendo profissionais e alunos do PURO/UFF e da PUC-Rio.
\item [Publicações:] Esperamos publicar os resultados do projeto em conferências como a \emph{Workshop em Tecnologia da Informação e da Linguagem Humana} (TIL), a \emph{AAAI Workshop on Explanation-aware Computing}, a \emph{International Workshop on Description Logics}, e a \emph{Conference on Automated Deduction} (CADE), assim como em periódicos especializados, como, por exemplo, o \emph{Applied Ontology}.
\end{description}
\section{Cronograma}
\label{sec-cron}
Este projeto se desenvolverá durante 2 anos, a partir de abril de 2007, segundo o cronograma da Figura~\ref{fig-cron}, na página~\pageref{fig-cron}.
\begin{sidewaysfigure}
\tiny
\begin{center}
\begin{tabular}{|p{.25\linewidth}|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|}
\hline
\multicolumn{1}{|r|}{Ano} &
\multicolumn{9}{c|}{2007} &
\multicolumn{12}{c|}{2008} &
\multicolumn{3}{c|}{2009} \\
\hline
\multicolumn{1}{|r|}{Mês} &
04 & 05 & 06 & 07 & 08 & 09 & 10 & 11 & 12 &
01 & 02 & 03 & 04 & 05 & 06 & 07 & 08 & 09 & 10 & 11 & 12 &
01 & 02 & 03 \\
\hline
\hline
\cronentry{Seleção de bolsistas} &
\x & % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Estudo da bibliografia básica} &
& % 04/07
\x & % 05/07
\x & % 06/07
\x & % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Instalação e estudo de ferramentas de \emph{software} para ontologias e DL} &
& % 04/07
\x & % 05/07
\x & % 06/07
\x & % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Estudo de diferentes cálculos dedutivos para DL e das relações entre eles} &
& % 04/07
& % 05/07
& % 06/07
\x & % 07/07
\x & % 08/07
\x & % 09/07
\x & % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Implementação de protótipos de provadores baseados em diferentes cálculos dedutivos} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
\x & % 10/07
\x & % 11/07
\x & % 12/07
\x & % 01/08
\x & % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Definição de mapeamentos entre provas em diferentes cálculos dedutivos} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
\x & % 10/07
\x & % 11/07
\x & % 12/07
\x & % 01/08
\x & % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Escolha ou definição de um cálculo dedutivo a partir do qual serão geradas explicações} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
\x & % 03/08
\x & % 04/08
\x & % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Definição do formalismo para representar explicações} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
\x & % 04/08
\x & % 05/08
\x & % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Projeto de algoritmos de geração de explicações} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
\x & % 06/08
\x & % 07/08
\x & % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Implementação de protótipo de um gerador de explicações} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
\x & % 08/08
\x & % 09/08
\x & % 10/08
\x & % 11/08
\x & % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Planejamento de experimentos de legibilidade e usabilidade} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
\x & % 10/08
\x & % 11/08
& % 12/08
& % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Realização de experimentos de legibilidade e usabilidade} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
\x & % 12/08
\x & % 01/09
& % 02/09
% 03/09
\\
\hline
\cronentry{Análise dos resultados dos experimentos} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
\x & % 01/09
\x & % 02/09
% 03/09
\\
\hline
\cronentry{Confecção de relatório final} &
& % 04/07
& % 05/07
& % 06/07
& % 07/07
& % 08/07
& % 09/07
& % 10/07
& % 11/07
& % 12/07
& % 01/08
& % 02/08
& % 03/08
& % 04/08
& % 05/08
& % 06/08
& % 07/08
& % 08/08
& % 09/08
& % 10/08
& % 11/08
& % 12/08
& % 01/09
\x & % 02/09
\x % 03/09
\\
\hline
\end{tabular}
\end{center}
\caption{Cronograma}
\label{fig-cron}
\end{sidewaysfigure}
\section{Equipe}
\label{sec-equipe}
\begin{itemize}
\item Pesquisador: Fernando Náufel do Amaral, D.Sc.
\item Bolsistas de iniciação científica: dois alunos de graduação em Ciência da Computação, com carga horária de 12~horas semanais cada um.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\bibliographystyle{babplain}
\bibliography{projetofnaufel2007}
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: