Projetos finalizados



Árvores de prova

Provador Automático que gera provas em forma de árvores. Não fica-se sabendo apenas a veracidade da consulta, mas também como essa veracidade foi comprovada. Possui implementação completa e relatório técnico. 

Sequoia

Provador automático de teoremas capaz de identificar falhas numa conjectura expressa em lógica de primeira ordem. Futuramente pretende-se criar uma nova versão capaz de propor correções para que falsas conjecturas se tornem teoremas. Possui implementação e artigo relacionado.

Provadores Baseados em Unificação com Sorts

Proposta de um algoritmo de unificação para termos de sorts. Com esse algoritmo, é possível inserir deduções na máquina de inferência e reduzir os espaço de busca para provadores automáticos. Possui descrição de uma linguagem declarativa de primeira ordem e implementação de um sistema de unificação que utiliza declarações.





Projetos futuros



Sequoia

Implementação de um sistema que, além de verificar a veracidade de uma conjectura, diz quais mudanças podem ser aplicadas nesta para que se torne um teorema, caso seja uma conjectura falsa.

Aspectos Pragmáticos do Uso de Lógica em Sistemas Baseados em Conhecimento



  • Explicações de respostas para usuários leigos (Vieira, 1988) (Coelho, 1989) (Vieira & Coelho, 1989) (Castilho, 1991) (Castilho & Vieira, 1991)

  • Auxílio ao entendimento de bases de conhecimento (Cohen, 1984) (Eisinger et alii, 1991)

  • Traduções prova-a-prova entre Resolução, Sistemas de Gentzen, Dedução Natural e Tableaux Semânticos (Fitting, 1996)

  • Controle de inferência recursiva (Smith et alii, 1986) (Vieira, 1989) (Lopes, 1991) (Lopes& Vieira, 1991)

  • Processamento de definições (Carvalho & Vieira, 1989)

  • Processamento de igualdade restrita (Carvalho & Vieira, 1989)

  • Preprocessamento de fórmulas (Rock, 1995) (Eisinger et alii, 1991) (Graf, 1992))





[Projetos] [Implementações] [Textos e Artigos] [Coordenadores] [Informações sobre o Laboratório] [downloads] [Links]

LInC