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 |
|
[Projetos] [Implementações] [Textos e Artigos] [Coordenadores] [Informações sobre o Laboratório] [downloads] [Links]