Dissertação

Raciocínio Abdutivo sobre Especificações de Agentes EVALUATED

O trabalho desenvolvido na presente dissertação insere-se na área de verificação de especificações formais de sistemas de agentes. Os objectivos da dissertação são, partindo do trabalhado apresentado em "Multi-agent system specification and certification" (P. Gouveia e J. Ramos, 2003), implementar a técnica de raciocínio abdutivo aí descrita para o caso de uma especificação de agente num contexto proposicional no sistema Mathematica, estender esta técnica a um fragmento da lógica de 1ª ordem e implementar esta extensão. Ao longo do trabalho usamos o cálculo de estados e situações para definir especificações de agentes. Quando uma certa propriedade do agente não pode ser inferida a partir da sua especificação, esta especificação tem de ser enriquecida com novas fórmulas adequadas. Designamos essa propriedade por problema de abdução, e as fórmulas geradas para enriquecer a especificação por explicações. No caso de uma especificação de agente num contexto proposicional iremos usar, como auxiliar das técnicas de raciocínio abdutivo, tableaux proposicionais. Porém, estes não serão suficientes ao considerarmos especificações num contexto de lógica de 1ª ordem, sendo complementados por técnicas de programação linear.
Especificação, certificação, abdução, cálculo de situações

Outubro 9, 2007, 14:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar

ORIENTADOR

Maria Paula Antunes Abrantes Gouveia

Departamento de Matemática (DM)

Professor Auxiliar